Grace/Cumulus/Algebra/LinearSpanMap.g17

Open in Workbench Download source

Imports

SpanProduct · Image

Declarations

• Submodule.comap theorem derivation
• linearSpan.map_mem theorem derivation

Source

1-- Transport of relative linear spans along algebra homomorphisms (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.LinearSpanMap8import SpanProduct9import Image1011section Algebras12variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e f g : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15notation ring U := (C, sum, o, inverse, product, e)16hypothesis coefficients : IsCommRing(R)17hypothesis source : IsCommRing(S)18hypothesis target : IsCommRing(U)19hypothesis coefficientMap : IsRingHom(f, R, S)20hypothesis hom : IsRingHom(g, S, U)2122theorem Submodule.comap (T : Set)23  requires submodule : Submodule(compose(g, f, A, B, C), R, U, T)24  shows Submodule(f, R, S, subringComap(g, B, T))25proof26  have ordinary := IsCommRing.ring with source27  have functionF := IsRingHom.function with coefficientMap28  have functionG := IsRingHom.function with hom29  have composite := IsRingHom.compose with coefficients, coefficientMap, hom30  have zeroIn := IsRing.zero_in_carrier with ordinary31  have zeroMem := Submodule.zero_mem with coefficients, target, composite, submodule32  have negClosed := Submodule.neg_closed with coefficients, target, composite, submodule33  have addClosed := Submodule.add_closed with coefficients, target, composite, submodule34  have zeroValue := IsRingHom.zero with hom35  have bounded : subringComap(g, B, T) ⊆ B by simp [Subset, subringComap.membership]36  have zeroMember : S[0] ∈ subringComap(g, B, T)37    apply subringComap.membership.backward38    rw zeroValue39    refine ⟨zeroIn, zeroMem⟩40  have negative : ClosedUnary(subringComap(g, B, T), minus)41    intros x hx42    obtain ⟨inB, member⟩ := subringComap.membership.forward with hx43    have closed := IsRing.neg_closed with ordinary, inB44    have mapped := IsRingHom.neg with hom, inB45    have result := ClosedUnary.mem with negClosed, member46    apply subringComap.membership.backward47    rw mapped48    refine ⟨closed, result⟩49  have addition : ClosedBinary(subringComap(g, B, T), plus)50    intros x hx y hy51    obtain ⟨inX, memberX⟩ := subringComap.membership.forward with hx52    obtain ⟨inY, memberY⟩ := subringComap.membership.forward with hy53    have closed := IsRing.add_closed with ordinary, inX, inY54    have mapped := IsRingHom.add with hom, inX, inY55    have result := ClosedBinary.mem with addClosed, memberX, memberY56    apply subringComap.membership.backward57    rw mapped58    refine ⟨closed, result⟩59  have scalars : ∀ a ∈ R, ∀ x ∈ subringComap(g, B, T), S[f(a) * x] ∈ subringComap(g, B, T)60    intros a ha x hx61    obtain ⟨inB, member⟩ := subringComap.membership.forward with hx62    have image := IsRingHom.closed with coefficientMap, ha63    have closed := IsRing.mul_closed with ordinary, image, inB64    have mapped := IsRingHom.mul with hom, image, inB65    have compositeValue := compose.apply with ha66    have result := Submodule.scalar_mul_mem with coefficients, target, composite, submodule, ha, member67    rw compositeValue at result68    apply subringComap.membership.backward69    rw mapped70    refine ⟨closed, result⟩71  unfold Submodule72  refine ⟨bounded, zeroMember, negative, addition, scalars⟩7374theorem linearSpan.map_mem (G x : Set)75  requires bounded : G ⊆ S76  requires member : x ∈ linearSpan(f, R, S, G)77  shows g(x) ∈ linearSpan(compose(g, f, A, B, C), R, U, functionImage(g, G, C))78proof79  have composite := IsRingHom.compose with coefficients, coefficientMap, hom80  have span := linearSpan.submodule at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), functionImage(g, G, C) with *81  have preimage := Submodule.comap with coefficients, source, target, coefficientMap, hom, span82  have imageBound : functionImage(g, G, C) ⊆ C by exact functionImage.subset at g, G, C83  have contains := linearSpan.contains with coefficients, target, composite, imageBound84  have generators : G ⊆ subringComap(g, B, linearSpan(compose(g, f, A, B, C), R, U, functionImage(g, G, C)))85    intros u hu86    have inB : u ∈ B by simp [Subset]87    have closed := IsRingHom.closed with hom, inB88    have image : g(u) ∈ functionImage(g, G, C) := functionImage.membership.backward with ⟨closed, u, hu, rfl⟩89    have inSpan : g(u) ∈ linearSpan(compose(g, f, A, B, C), R, U, functionImage(g, G, C)) by simp [Subset]90    exact subringComap.membership.backward with ⟨inB, inSpan⟩91  have included := linearSpan.least with coefficients, source, coefficientMap, preimage, generators92  have inPreimage := included with x, member93  have data := subringComap.membership.forward with inPreimage94  exact data.right9596end Algebras97