Grace/Cumulus/Algebra/FiniteModuleTower.g17

Open in Workbench Download source

Imports

LinearSpanMap

Declarations

Source

1-- Finite modules compose in a tower of commutative algebras (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.FiniteModuleTower8import LinearSpanMap910section Algebras11variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e f g : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14notation ring U := (C, sum, o, inverse, product, e)15hypothesis coefficients : IsCommRing(R)16hypothesis source : IsCommRing(S)17hypothesis target : IsCommRing(U)18hypothesis coefficientMap : IsRingHom(f, R, S)19hypothesis hom : IsRingHom(g, S, U)2021theorem linearSpan.tower_generators (G H : Set)22  requires boundedG : G ⊆ S23  requires boundedH : H ⊆ U24  requires spansG : linearSpan(f, R, S, G) = S25  requires spansH : linearSpan(g, S, U, H) = U26  shows linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H)) = U27proof28  have composite := IsRingHom.compose with coefficients, coefficientMap, hom29  have ordinaryS := IsCommRing.ring with source30  have ordinaryU := IsCommRing.ring with target31  have multiplicative := IsRing.multiplicative with ordinaryS32  have oneIn := IsMonoid.unit_in_carrier with multiplicative33  have oneValue := IsRingHom.one with hom34  have imageBound : functionImage(g, G, C) ⊆ U by exact functionImage.subset at g, G, C35  have productsBound := spanProducts.subset at C, product, functionImage(g, G, C), H36  have span := linearSpan.submodule at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), spanProducts(U, functionImage(g, G, C), H) with *37  have spanBound := Submodule.subset with coefficients, target, composite, span38  have spanZero := Submodule.zero_mem with coefficients, target, composite, span39  have spanNeg := Submodule.neg_closed with coefficients, target, composite, span40  have spanAdd := Submodule.add_closed with coefficients, target, composite, span41  have containsH := linearSpan.contains at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), H with *42  have mappedSpan : ∀ b ∈ S, g(b) ∈ linearSpan(compose(g, f, A, B, C), R, U, functionImage(g, G, C))43    intros b hb44    have member : b ∈ linearSpan(f, R, S, G) by rwa spansG45    exact linearSpan.map_mem with coefficients, source, target, coefficientMap, hom, boundedG, member46  have scalars : ∀ b ∈ S, ∀ x ∈ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H)), U[g(b) * x] ∈ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H))47    intros b hb x hx48    have imageB := IsRingHom.closed with hom, hb49    have generators : ∀ p ∈ spanProducts(U, functionImage(g, G, C), H), U[p * g(b)] ∈ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H))50      intros p hp51      obtain ⟨inP, a, ha, v, hv, valueP⟩ := spanProducts.membership.forward with hp52      obtain ⟨inA, u, hu, valueA⟩ := functionImage.membership.forward with ha53      have inU : u ∈ S by simp [Subset]54      have inV : v ∈ U by simp [Subset]55      have inSpanV : v ∈ linearSpan(compose(g, f, A, B, C), R, U, H) by simp [Subset]56      have imageU := IsRingHom.closed with hom, inU57      have closed := IsRing.mul_closed with ordinaryS, hb, inU58      have first := mappedSpan with S[b * u], closed59      have member := linearSpan.product_mem with coefficients, target, composite, imageBound, boundedH, first, inSpanV60      have mapped := IsRingHom.mul with hom, hb, inU61      rw mapped at member62      have equation : U[(g(u) * v) * g(b)] = U[(g(b) * g(u)) * v] by ring63      rwa [valueP, valueA, equation]64    have multiplied := linearSpan.mul_mem with coefficients, target, composite, span, productsBound, generators, hx65    have inX : x ∈ U by simp [Subset]66    have commute : U[g(b) * x] = U[x * g(b)] by ring67    rwa commute68  have overS : Submodule(g, S, U, linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H)))69    unfold Submodule70    refine ⟨spanBound, spanZero, spanNeg, spanAdd, scalars⟩71  have generators : H ⊆ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H))72    intros v hv73    have inV : v ∈ U by simp [Subset]74    have inSpanV : v ∈ linearSpan(compose(g, f, A, B, C), R, U, H) by simp [Subset]75    have first := mappedSpan with unit, oneIn76    have member := linearSpan.product_mem with coefficients, target, composite, imageBound, boundedH, first, inSpanV77    rw oneValue at member78    have equation : U[1 * v] = v by ring79    rwa equation at member80  have whole := linearSpan.least with source, target, hom, overS, generators81  rw spansH at whole82  exact Subset.antisymmetric with spanBound, whole8384theorem FiniteAlgebraModule.tower85  requires finiteS : FiniteAlgebraModule(f, R, S)86  requires finiteU : FiniteAlgebraModule(g, S, U)87  shows FiniteAlgebraModule(compose(g, f, A, B, C), R, U)88proof89  obtain ⟨G, finiteG, boundedG, spansG⟩ := finiteS90  obtain ⟨H, finiteH, boundedH, spansH⟩ := finiteU91  have composite := IsRingHom.compose with coefficients, coefficientMap, hom92  have function := IsRingHom.function with hom93  have finiteImage := Finite.function_image with function, finiteG, boundedG94  have imageBound : functionImage(g, G, C) ⊆ U by exact functionImage.subset at g, G, C95  have finite := spanProducts.finite with coefficients, target, composite, finiteImage, finiteH, imageBound, boundedH96  have bounded := spanProducts.subset at C, product, functionImage(g, G, C), H97  have spans := linearSpan.tower_generators with coefficients, source, target, coefficientMap, hom, boundedG, boundedH, spansG, spansH98  unfold FiniteAlgebraModule99  refine ⟨spanProducts(U, functionImage(g, G, C), H), finite, bounded, spans⟩100101end Algebras102