Grace/Cumulus/Algebra/SpanInsert.g17

Open in Workbench Download source

Imports

LinearSpan

Declarations

Source

1-- Coefficient witnesses for adjoining a generator to a linear span (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.SpanInsert8import LinearSpan910def scalarExtension (f A B plus times M x : Set) : Set :=11  {y ∈ B | ∃ a ∈ A, ∃ u ∈ M, y = plus(times(f(a), x), u)}1213section Algebras14variable (A add zero neg mul one B plus z minus times unit f M x : Set)15notation ring R := (A, add, zero, neg, mul, one)16notation ring S := (B, plus, z, minus, times, unit)17hypothesis source : IsCommRing(R)18hypothesis target : IsCommRing(S)19hypothesis hom : IsRingHom(f, R, S)20hypothesis submodule : Submodule(f, R, S, M)21hypothesis element : x ∈ S2223theorem scalarExtension.submodule24  shows Submodule(f, R, S, scalarExtension(f, A, B, plus, times, M, x))25proof26  have r := IsCommRing.ring with source27  have s := IsCommRing.ring with target28  have sourceZero := IsRing.zero_in_carrier with r29  have targetZero := IsRing.zero_in_carrier with s30  have zeroMem := Submodule.zero_mem with source, target, hom, submodule31  have boundedM := Submodule.subset with source, target, hom, submodule32  have negM := Submodule.neg_closed with source, target, hom, submodule33  have addM := Submodule.add_closed with source, target, hom, submodule34  have bounded : scalarExtension(f, A, B, plus, times, M, x) ⊆ S by simp [Subset, scalarExtension]35  have zeroMember : S[0] ∈ scalarExtension(f, A, B, plus, times, M, x)36    apply scalarExtension.membership.backward37    refine ⟨targetZero, zero, sourceZero, z, zeroMem, ?_⟩38    have mapped := IsRingHom.zero with hom39    rw mapped40    ring41  have negative : ClosedUnary(scalarExtension(f, A, B, plus, times, M, x), minus)42    intros y hy43    obtain ⟨member, a, ha, u, hu, equation⟩ := scalarExtension.membership.forward with hy44    have negativeY := IsRing.neg_closed with s, member45    have negativeA := IsRing.neg_closed with r, ha46    have negativeU := ClosedUnary.mem with negM, hu47    have inB : u ∈ S by exact boundedM with u, hu48    have image := IsRingHom.closed with hom, ha49    apply scalarExtension.membership.backward50    refine ⟨negativeY, R[-a], negativeA, S[-u], negativeU, ?_⟩51    have mapped := IsRingHom.neg with hom, ha52    rw [mapped, equation]53    ring54  have addition : ClosedBinary(scalarExtension(f, A, B, plus, times, M, x), plus)55    intros y hy w hw56    obtain ⟨memberY, a, ha, u, hu, equationY⟩ := scalarExtension.membership.forward with hy57    obtain ⟨memberW, b, hb, v, hv, equationW⟩ := scalarExtension.membership.forward with hw58    have sum := IsRing.add_closed with s, memberY, memberW59    have coefficient := IsRing.add_closed with r, ha, hb60    have remainder := ClosedBinary.mem with addM, hu, hv61    have inB : u ∈ S ∧ v ∈ S62      have first := boundedM with u, hu63      have second := boundedM with v, hv64      refine ⟨first, second⟩65    have memberU := inB.left66    have memberV := inB.right67    have imageA := IsRingHom.closed with hom, ha68    have imageB := IsRingHom.closed with hom, hb69    apply scalarExtension.membership.backward70    refine ⟨sum, R[a + b], coefficient, S[u + v], remainder, ?_⟩71    have mapped := IsRingHom.add with hom, ha, hb72    rw [mapped, equationY, equationW]73    ring74  have scalars : ∀ c ∈ R, ∀ y ∈ scalarExtension(f, A, B, plus, times, M, x), S[f(c) * y] ∈ scalarExtension(f, A, B, plus, times, M, x)75    intros c hc y hy76    obtain ⟨member, a, ha, u, hu, equation⟩ := scalarExtension.membership.forward with hy77    have imageC := IsRingHom.closed with hom, hc78    have imageA := IsRingHom.closed with hom, ha79    have product := IsRing.mul_closed with s, imageC, member80    have coefficient := IsRing.mul_closed with r, hc, ha81    have remainder := Submodule.scalar_mul_mem with source, target, hom, submodule, hc, hu82    have inB : u ∈ S by exact boundedM with u, hu83    apply scalarExtension.membership.backward84    refine ⟨product, R[c * a], coefficient, S[f(c) * u], remainder, ?_⟩85    have mapped := IsRingHom.mul with hom, hc, ha86    rw [mapped, equation]87    ring88  unfold Submodule89  refine ⟨bounded, zeroMember, negative, addition, scalars⟩9091theorem scalarExtension.contains92  shows insert(x, M) ⊆ scalarExtension(f, A, B, plus, times, M, x)93proof94  have r := IsCommRing.ring with source95  have s := IsCommRing.ring with target96  have zeroIn := IsRing.zero_in_carrier with r97  have oneIn : R[1] ∈ R by typecheck98  have zeroMem := Submodule.zero_mem with source, target, hom, submodule99  have bound := Submodule.subset with source, target, hom, submodule100  intros y hy101  have alternatives := insert.membership.forward with hy102  cases alternatives with equal | old103  . rw equal104    apply scalarExtension.membership.backward105    refine ⟨element, one, oneIn, z, zeroMem, ?_⟩106    have mapped := IsRingHom.one with hom107    rw mapped108    ring109  . have member : y ∈ S110      exact bound with y, old111    apply scalarExtension.membership.backward112    refine ⟨member, zero, zeroIn, y, old, ?_⟩113    have mapped := IsRingHom.zero with hom114    rw mapped115    ring116117end Algebras118119section Spans120variable (A add zero neg mul one B plus z minus times unit f G x : Set)121notation ring R := (A, add, zero, neg, mul, one)122notation ring S := (B, plus, z, minus, times, unit)123hypothesis source : IsCommRing(R)124hypothesis target : IsCommRing(S)125hypothesis hom : IsRingHom(f, R, S)126hypothesis bounded : G ⊆ S127hypothesis element : x ∈ S128129theorem linearSpan.insert130  shows linearSpan(f, R, S, insert(x, G)) = scalarExtension(f, A, B, plus, times, linearSpan(f, R, S, G), x)131proof132  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *133  have extension := scalarExtension.submodule with source, target, hom, span, element134  have contains := scalarExtension.contains with source, target, hom, span, element135  have oldContains := linearSpan.contains with source, target, hom, bounded136  have generators : insert(x, G) ⊆ scalarExtension(f, A, B, plus, times, linearSpan(f, R, S, G), x)137    simp138  have first := linearSpan.least with source, target, hom, extension, generators139  have enlarged := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, insert(x, G) with *140  have bound : insert(x, G) ⊆ S by simp [Subset, insert.membership]141  have included := linearSpan.contains with source, target, hom, bound142  have xIn : x ∈ linearSpan(f, R, S, insert(x, G)) by settle with Subset, insert.membership143  have old : G ⊆ insert(x, G) by simp [Subset, insert.membership]144  have oldSpan := linearSpan.mono with source, target, hom, bound, old145  have addClosed := Submodule.add_closed with source, target, hom, enlarged146  have second : scalarExtension(f, A, B, plus, times, linearSpan(f, R, S, G), x) ⊆ linearSpan(f, R, S, insert(x, G))147    intros y hy148    obtain ⟨member, a, ha, u, hu, equation⟩ := scalarExtension.membership.forward with hy149    have scalar := Submodule.scalar_mul_mem with source, target, hom, enlarged, ha, xIn150    have rest : u ∈ linearSpan(f, R, S, insert(x, G)) by exact oldSpan with u, hu151    rw equation152    exact ClosedBinary.mem with addClosed, scalar, rest153  exact Subset.antisymmetric with first, second154155theorem linearSpan.insert_membership (y : Set)156  shows y ∈ linearSpan(f, R, S, insert(x, G)) ↔157    y ∈ S ∧ (∃ a ∈ R, ∃ u ∈ linearSpan(f, R, S, G), y = S[f(a) * x + u])158proof159  have equation := linearSpan.insert with source, target, hom, bounded, element160  rw equation161  exact scalarExtension.membership162163end Spans164section EmptySpan165variable (A add zero neg mul one B plus z minus times unit f : Set)166notation ring R := (A, add, zero, neg, mul, one)167notation ring S := (B, plus, z, minus, times, unit)168hypothesis source : IsCommRing(R)169hypothesis target : IsCommRing(S)170hypothesis hom : IsRingHom(f, R, S)171172theorem Submodule.zero173  shows Submodule(f, R, S, {S[0]})174proof175  have ordinary := IsCommRing.ring with target176  have zeroIn := IsRing.zero_in_carrier with ordinary177  have bounded : {S[0]} ⊆ S by simp [Subset, singleton.membership]178  have zeroMember : S[0] ∈ {S[0]} by simp [singleton.membership]179  have negative : ClosedUnary({S[0]}, minus)180    intros u hu181    have equal := singleton.membership.forward with hu182    rw equal183    have value : S[-0] = S[0] by ring184    rwa value185  have addition : ClosedBinary({S[0]}, plus)186    intros u hu v hv187    have first := singleton.membership.forward with hu188    have second := singleton.membership.forward with hv189    rw [first, second]190    have value : S[0 + 0] = S[0] by ring191    rwa value192  have scalars : ∀ a ∈ R, ∀ u ∈ {S[0]}, S[f(a) * u] ∈ {S[0]}193    intros a ha u hu194    have image := IsRingHom.closed with hom, ha195    have equal := singleton.membership.forward with hu196    rw equal197    have value : S[f(a) * 0] = S[0] by ring198    rwa value199  unfold Submodule200  refine ⟨bounded, zeroMember, negative, addition, scalars⟩201202theorem linearSpan.empty203  shows linearSpan(f, R, S, ∅) = {S[0]}204proof205  have zeroModule := Submodule.zero with *206  have empty := empty.subset at {S[0]}207  have first := linearSpan.least with source, target, hom, zeroModule, empty208  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, ∅ with *209  have zeroMember := Submodule.zero_mem with source, target, hom, span210  have second : {S[0]} ⊆ linearSpan(f, R, S, ∅)211    intros y hy212    have equal := singleton.membership.forward with hy213    rwa equal214  exact Subset.antisymmetric with first, second215216end EmptySpan217