Grace/Cumulus/Algebra/SpanProduct.g17

Open in Workbench Download source

Imports

LinearSpanMultiplication · Cardinal.FiniteImage · Cardinal.Product

Declarations

Source

1-- Products of spanning sets in a commutative algebra (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.SpanProduct8import LinearSpanMultiplication9import Cardinal.FiniteImage10import Cardinal.Product1112def spanProducts (B times G H : Set) : Set := functionImage(times, G × H, B)1314notation scoped spanProducts(R, G, H) => spanProducts(R.carrier, R.mul, G, H)1516theorem spanProducts.membership (B times G H w : Set)17  shows w ∈ spanProducts(B, times, G, H) ↔ w ∈ B ∧ (∃ g ∈ G, ∃ h ∈ H, w = times(g, h))18proof19  constructor20  . intro member21    unfold spanProducts at member22    obtain ⟨inB, p, hp, value⟩ := functionImage.membership.forward with member23    obtain ⟨bound, g, hg, h, hh, shape⟩ := product.membership.forward with hp24    rw shape at value25    have equation : w = times(g, h)26      simp [call2]27    refine ⟨inB, g, hg, h, hh, equation⟩28  . intro data29    obtain ⟨inB, g, hg, h, hh, value⟩ := data30    unfold call2 at value31    have pair := product.pair with hg, hh32    unfold spanProducts33    exact functionImage.membership.backward with ⟨inB, (g, h), pair, value⟩3435theorem spanProducts.subset (B times G H : Set)36  shows spanProducts(B, times, G, H) ⊆ B37proof38  simp3940section Algebras41variable (A add zero neg mul one B plus z minus times unit f : Set)42notation ring R := (A, add, zero, neg, mul, one)43notation ring S := (B, plus, z, minus, times, unit)44hypothesis source : IsCommRing(R)45hypothesis target : IsCommRing(S)46hypothesis hom : IsRingHom(f, R, S)4748theorem spanProducts.finite (G H : Set)49  requires finiteG : Finite(G)50  requires finiteH : Finite(H)51  requires boundedG : G ⊆ S52  requires boundedH : H ⊆ S53  shows Finite(spanProducts(B, times, G, H))54proof55  have function : times : B × B → B by simp [IsCommRing, IsRing, IsMonoid, IsSemigroup, IsMagma]56  have finite := Finite.product with finiteG, finiteH57  have bounded := product.monotone with boundedG, boundedH58  unfold spanProducts59  exact Finite.function_image with function, finite, bounded6061theorem linearSpan.mul_mem_of_generators (G H T u v : Set)62  requires boundedG : G ⊆ S63  requires boundedH : H ⊆ S64  requires submodule : Submodule(f, R, S, T)65  requires products : ∀ g ∈ G, ∀ h ∈ H, S[g * h] ∈ T66  requires memberU : u ∈ linearSpan(f, R, S, G)67  requires memberV : v ∈ linearSpan(f, R, S, H)68  shows S[u * v] ∈ T69proof70  have spanH := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, H with *71  have inV : v ∈ S by simp [Subset]72  have generators : ∀ g ∈ G, S[g * v] ∈ T73    intros g hg74    have inG : g ∈ S by simp [Subset]75    have right : ∀ h ∈ H, S[h * g] ∈ T76      intros h hh77      have inH : h ∈ S by simp [Subset]78      have product := products with g, hg, h, hh79      have commute : S[h * g] = S[g * h] by ring80      rwa commute81    have product := linearSpan.mul_mem with source, target, hom, submodule, inG, boundedH, right, memberV82    have commute : S[g * v] = S[v * g] by ring83    rwa commute84  exact linearSpan.mul_mem with source, target, hom, submodule, inV, boundedG, generators, memberU8586theorem linearSpan.product_mem (G H u v : Set)87  requires boundedG : G ⊆ S88  requires boundedH : H ⊆ S89  requires memberU : u ∈ linearSpan(f, R, S, G)90  requires memberV : v ∈ linearSpan(f, R, S, H)91  shows S[u * v] ∈ linearSpan(f, R, S, spanProducts(B, times, G, H))92proof93  have ordinary := IsCommRing.ring with target94  have bounded := spanProducts.subset at B, times, G, H95  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, spanProducts(B, times, G, H) with *96  have contains := linearSpan.contains with source, target, hom, bounded97  have products : ∀ g ∈ G, ∀ h ∈ H, S[g * h] ∈ linearSpan(f, R, S, spanProducts(B, times, G, H))98    intros g hg h hh99    have inG : g ∈ S by simp [Subset]100    have inH : h ∈ S by simp [Subset]101    have closed := IsRing.mul_closed with ordinary, inG, inH102    have member : S[g * h] ∈ spanProducts(B, times, G, H)103      exact spanProducts.membership.backward with ⟨closed, g, hg, h, hh, rfl⟩104    exact contains with S[g * h], member105  exact linearSpan.mul_mem_of_generators with source, target, hom, boundedG, boundedH, span, products, memberU, memberV106107theorem linearSpan.product_subalgebra (G H : Set)108  requires boundedG : G ⊆ S109  requires boundedH : H ⊆ S110  requires algebraG : Subalgebra(f, R, S, linearSpan(f, R, S, G))111  requires algebraH : Subalgebra(f, R, S, linearSpan(f, R, S, H))112  shows Subalgebra(f, R, S, linearSpan(f, R, S, spanProducts(B, times, G, H)))113proof114  have ordinary := IsCommRing.ring with target115  have ringG := Subalgebra.subring with source, target, hom, algebraG116  have ringH := Subalgebra.subring with source, target, hom, algebraH117  have oneG := IsSubring.one_closed with ringG118  have oneH := IsSubring.one_closed with ringH119  have mulG := IsSubring.mul_closed with ringG120  have mulH := IsSubring.mul_closed with ringH121  have containsG := linearSpan.contains with source, target, hom, boundedG122  have containsH := linearSpan.contains with source, target, hom, boundedH123  have bounded := spanProducts.subset at B, times, G, H124  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, spanProducts(B, times, G, H) with *125  have bound := Submodule.subset with source, target, hom, span126  have zeroMem := Submodule.zero_mem with source, target, hom, span127  have negative := Submodule.neg_closed with source, target, hom, span128  have addition := Submodule.add_closed with source, target, hom, span129  have multiplicative := IsRing.multiplicative with ordinary130  have unitIn := IsMonoid.unit_in_carrier with multiplicative131  have unitProduct := linearSpan.product_mem with source, target, hom, boundedG, boundedH, oneG, oneH132  have unitEquation : S[1 * 1] = S[1] by ring133  rw unitEquation at unitProduct134  have products : ∀ p ∈ spanProducts(B, times, G, H), ∀ q ∈ spanProducts(B, times, G, H), S[p * q] ∈ linearSpan(f, R, S, spanProducts(B, times, G, H))135    intros p hp q hq136    obtain ⟨pIn, g, hg, h, hh, pValue⟩ := spanProducts.membership.forward with hp137    obtain ⟨qIn, k, hk, l, hl, qValue⟩ := spanProducts.membership.forward with hq138    have gIn : g ∈ S by simp [Subset]139    have hIn : h ∈ S by simp [Subset]140    have kIn : k ∈ S by simp [Subset]141    have lIn : l ∈ S by simp [Subset]142    have gSpan : g ∈ linearSpan(f, R, S, G) by simp [Subset]143    have kSpan : k ∈ linearSpan(f, R, S, G) by simp [Subset]144    have hSpan : h ∈ linearSpan(f, R, S, H) by simp [Subset]145    have lSpan : l ∈ linearSpan(f, R, S, H) by simp [Subset]146    have first := ClosedBinary.mem with mulG, gSpan, kSpan147    have second := ClosedBinary.mem with mulH, hSpan, lSpan148    have member := linearSpan.product_mem with source, target, hom, boundedG, boundedH, first, second149    have equation : S[(g * h) * (k * l)] = S[(g * k) * (h * l)] by ring150    rwa [pValue, qValue, equation]151  have multiplication : ClosedBinary(linearSpan(f, R, S, spanProducts(B, times, G, H)), times)152    intros u hu v hv153    exact linearSpan.mul_mem_of_generators with source, target, hom, bounded, bounded, span, products, hu, hv154  have subring : IsSubring(S, linearSpan(f, R, S, spanProducts(B, times, G, H)))155    unfold IsSubring156    refine ⟨bound, zeroMem, unitProduct, negative, addition, multiplication⟩157  have coefficients : functionImage(f, R, S) ⊆ linearSpan(f, R, S, spanProducts(B, times, G, H))158    intros b hb159    obtain ⟨bIn, a, ha, equation⟩ := functionImage.membership.forward with hb160    have image := IsRingHom.closed with hom, ha161    have scalar := Submodule.scalar_mul_mem with source, target, hom, span, ha, unitProduct162    have value : S[f(a) * 1] = f(a) by ring163    rw value at scalar164    rwa equation165  unfold Subalgebra166  refine ⟨subring, coefficients⟩167168theorem linearSpan.product_adjoin (G H U V : Set)169  requires boundedG : G ⊆ S170  requires boundedH : H ⊆ S171  requires boundedU : U ⊆ S172  requires boundedV : V ⊆ S173  requires spansG : linearSpan(f, R, S, G) = algebraAdjoin(f, R, S, U)174  requires spansH : linearSpan(f, R, S, H) = algebraAdjoin(f, R, S, V)175  shows linearSpan(f, R, S, spanProducts(B, times, G, H)) = algebraAdjoin(f, R, S, U ∪ V)176proof177  have ordinary := IsCommRing.ring with target178  have algebraU := algebraAdjoin.subalgebra with source, target, hom, boundedU179  have algebraV := algebraAdjoin.subalgebra with source, target, hom, boundedV180  have algebraG := algebraU181  have algebraH := algebraV182  rw ← spansG at algebraG183  rw ← spansH at algebraH184  have generated := linearSpan.product_subalgebra with source, target, hom, boundedG, boundedH, algebraG, algebraH185  have ringG := Subalgebra.subring with source, target, hom, algebraG186  have ringH := Subalgebra.subring with source, target, hom, algebraH187  have unitG := IsSubring.one_closed with ringG188  have unitH := IsSubring.one_closed with ringH189  have containsU := algebraAdjoin.contains with source, target, hom, boundedU190  have containsV := algebraAdjoin.contains with source, target, hom, boundedV191  rw ← spansG at containsU192  rw ← spansH at containsV193  have generators : U ∪ V ⊆ linearSpan(f, R, S, spanProducts(B, times, G, H))194    intros u hu195    have casesU := union2.membership.forward with hu196    cases casesU with left | right197    . have inB : u ∈ S198        simp199      have member : u ∈ linearSpan(f, R, S, G) by simp [Subset]200      have product := linearSpan.product_mem with source, target, hom, boundedG, boundedH, member, unitH201      have equation : S[u * 1] = u by ring202      rwa equation at product203    . have inB : u ∈ S204        simp205      have member : u ∈ linearSpan(f, R, S, H) by simp [Subset]206      have product := linearSpan.product_mem with source, target, hom, boundedG, boundedH, unitG, member207      have equation : S[1 * u] = u by ring208      rwa equation at product209  have first := algebraAdjoin.least with source, target, hom, generated, generators210  have unionBound : U ∪ V ⊆ S by simp [Subset, union2.membership]211  have unionAlgebra := algebraAdjoin.subalgebra with source, target, hom, unionBound212  have unionModule := Subalgebra.submodule with source, target, hom, unionAlgebra213  have unionRing := Subalgebra.subring with source, target, hom, unionAlgebra214  have multiplication := IsSubring.mul_closed with unionRing215  have subsetU := union2.subset_left at U, V216  have subsetV := union2.subset_right at U, V217  have includedU := algebraAdjoin.mono with source, target, hom, subsetU218  have includedV := algebraAdjoin.mono with source, target, hom, subsetV219  have containsG := linearSpan.contains with source, target, hom, boundedG220  have containsH := linearSpan.contains with source, target, hom, boundedH221  rw spansG at containsG222  rw spansH at containsH223  have inUnionG := Subset.transitive with containsG, includedU224  have inUnionH := Subset.transitive with containsH, includedV225  have products : spanProducts(B, times, G, H) ⊆ algebraAdjoin(f, R, S, U ∪ V)226    intros p hp227    obtain ⟨pIn, g, hg, h, hh, value⟩ := spanProducts.membership.forward with hp228    have memberG : g ∈ algebraAdjoin(f, R, S, U ∪ V) by simp [Subset]229    have memberH : h ∈ algebraAdjoin(f, R, S, U ∪ V) by simp [Subset]230    rw value231    exact ClosedBinary.mem with multiplication, memberG, memberH232  have second := linearSpan.least with source, target, hom, unionModule, products233  exact Subset.antisymmetric with second, first234235end Algebras236