Grace/Cumulus/Algebra/LinearSpan.g17

Open in Workbench Download source

Imports

Adjoin

Declarations

Source

1-- Linear spans inside an algebra, relative to its coefficient homomorphism (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.LinearSpan8import Adjoin910predicate Submodule (f A B plus z minus times T : Set) :=11  T ⊆ B ∧ z ∈ T ∧ ClosedUnary(T, minus) ∧ ClosedBinary(T, plus) ∧12  (∀ a ∈ A, ∀ x ∈ T, times(f(a), x) ∈ T)1314notation scoped Submodule(f, R, S, T) => Submodule(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, T)1516def linearSpan (f A B plus z minus times G : Set) : Set :=17  {x ∈ B | ∀ T, Submodule(f, A, B, plus, z, minus, times, T) → G ⊆ T → x ∈ T}1819notation scoped linearSpan(f, R, S, G) => linearSpan(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, G)2021predicate FiniteAlgebraModule (f A B plus z minus times : Set) :=22  ∃ G, Finite(G) ∧ G ⊆ B ∧ linearSpan(f, A, B, plus, z, minus, times, G) = B2324notation scoped FiniteAlgebraModule(f, R, S) => FiniteAlgebraModule(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul)2526section Algebras27variable (A add zero neg mul one B plus z minus times unit f : Set)28notation ring R := (A, add, zero, neg, mul, one)29notation ring S := (B, plus, z, minus, times, unit)30hypothesis source : IsCommRing(R)31hypothesis target : IsCommRing(S)32hypothesis hom : IsRingHom(f, R, S)3334theorem Submodule.subset (T : Set)35  requires submodule : Submodule(f, R, S, T)36  shows T ⊆ B37proof38  simp [Submodule]3940theorem Submodule.zero_mem (T : Set)41  requires submodule : Submodule(f, R, S, T)42  shows S[0] ∈ T43proof44  simp [Submodule]4546theorem Submodule.neg_closed (T : Set)47  requires submodule : Submodule(f, R, S, T)48  shows ClosedUnary(T, minus)49proof50  simp [Submodule]5152theorem Submodule.add_closed (T : Set)53  requires submodule : Submodule(f, R, S, T)54  shows ClosedBinary(T, plus)55proof56  simp [Submodule]5758theorem Submodule.scalar_closed (T : Set)59  requires submodule : Submodule(f, R, S, T)60  shows ∀ a ∈ R, ∀ x ∈ T, S[f(a) * x] ∈ T61proof62  simp [Submodule]6364theorem Submodule.scalar_mul_mem (T a x : Set)65  requires submodule : Submodule(f, R, S, T)66  requires coefficient : a ∈ R67  requires member : x ∈ T68  shows S[f(a) * x] ∈ T69proof70  have closed := Submodule.scalar_closed with *71  exact closed with a, coefficient, x, member7273theorem Subalgebra.submodule (T : Set)74  requires subalgebra : Subalgebra(f, R, S, T)75  shows Submodule(f, R, S, T)76proof77  have subring := Subalgebra.subring with source, target, hom, subalgebra78  have bounded := IsSubring.subset_carrier with subring79  have zeroMember := IsSubring.zero_closed with subring80  have negative := IsSubring.neg_closed with subring81  have addition := IsSubring.add_closed with subring82  have scalars : ∀ a ∈ R, ∀ x ∈ T, S[f(a) * x] ∈ T83    intros a ha x hx84    exact Subalgebra.scalar_mul_mem with *85  unfold Submodule86  refine ⟨bounded, zeroMember, negative, addition, scalars⟩8788theorem linearSpan.mem_iff (G x : Set)89  shows x ∈ linearSpan(f, R, S, G) ↔ x ∈ S ∧ (∀ T, Submodule(f, R, S, T) → G ⊆ T → x ∈ T)90proof91  simp9293theorem linearSpan.subset (G : Set)94  shows linearSpan(f, R, S, G) ⊆ S95proof96  simp9798theorem linearSpan.contains (G : Set)99  requires bounded : G ⊆ S100  shows G ⊆ linearSpan(f, R, S, G)101proof102  intros x hx103  apply linearSpan.mem_iff.backward with source, target, hom104  constructor105  . exact bounded with x, hx106  . intros T submodule included107    exact included with x, hx108109theorem linearSpan.least (G T : Set)110  requires submodule : Submodule(f, R, S, T)111  requires generators : G ⊆ T112  shows linearSpan(f, R, S, G) ⊆ T113proof114  intros x hx115  have data := linearSpan.mem_iff.forward with *116  exact data.right with T, submodule, generators117118theorem linearSpan.submodule (G : Set)119  shows Submodule(f, R, S, linearSpan(f, R, S, G))120proof121  have ordinary := IsCommRing.ring with target122  have zeroIn := IsRing.zero_in_carrier with ordinary123  have bounded := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *124  have zeroMember : S[0] ∈ linearSpan(f, R, S, G)125    apply linearSpan.mem_iff.backward with source, target, hom126    refine ⟨zeroIn, ?_⟩127    intros T submodule generators128    exact Submodule.zero_mem with source, target, hom, submodule129  have negative : ClosedUnary(linearSpan(f, R, S, G), minus)130    intros x hx131    have data := linearSpan.mem_iff.forward with hx132    have closed := IsRing.neg_closed with ordinary, data.left133    apply linearSpan.mem_iff.backward with source, target, hom134    refine ⟨closed, ?_⟩135    intros T submodule generators136    have member := data.right with T, submodule, generators137    have closure := Submodule.neg_closed with source, target, hom, submodule138    exact ClosedUnary.mem with closure, member139  have addition : ClosedBinary(linearSpan(f, R, S, G), plus)140    intros x hx y hy141    have first := linearSpan.mem_iff.forward with hx142    have second := linearSpan.mem_iff.forward with hy143    have closed := IsRing.add_closed with ordinary, first.left, second.left144    apply linearSpan.mem_iff.backward with source, target, hom145    refine ⟨closed, ?_⟩146    intros T submodule generators147    have memberX := first.right with T, submodule, generators148    have memberY := second.right with T, submodule, generators149    have closure := Submodule.add_closed with source, target, hom, submodule150    exact ClosedBinary.mem with closure, memberX, memberY151  have scalars : ∀ a ∈ R, ∀ x ∈ linearSpan(f, R, S, G), S[f(a) * x] ∈ linearSpan(f, R, S, G)152    intros a ha x hx153    have data := linearSpan.mem_iff.forward with hx154    have image := IsRingHom.closed with hom, ha155    have closed := IsRing.mul_closed with ordinary, image, data.left156    apply linearSpan.mem_iff.backward with source, target, hom157    refine ⟨closed, ?_⟩158    intros T submodule generators159    have member := data.right with T, submodule, generators160    exact Submodule.scalar_mul_mem with source, target, hom, submodule, ha, member161  unfold Submodule162  refine ⟨bounded, zeroMember, negative, addition, scalars⟩163164theorem linearSpan.mono (G H : Set)165  requires bounded : H ⊆ S166  requires included : G ⊆ H167  shows linearSpan(f, R, S, G) ⊆ linearSpan(f, R, S, H)168proof169  have generated := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, H with *170  have contains := linearSpan.contains with *171  have generators := Subset.transitive with included, contains172  exact linearSpan.least with source, target, hom, generated, generators173174theorem linearSpan.eq_of_submodule (T : Set)175  requires submodule : Submodule(f, R, S, T)176  shows linearSpan(f, R, S, T) = T177proof178  have bounded := Submodule.subset with source, target, hom, submodule179  have reflexive := Subset.reflexive at T180  have first := linearSpan.least with source, target, hom, submodule, reflexive181  have second := linearSpan.contains with source, target, hom, bounded182  exact Subset.antisymmetric with first, second183184theorem linearSpan.idempotent (G : Set)185  shows linearSpan(f, R, S, linearSpan(f, R, S, G)) = linearSpan(f, R, S, G)186proof187  have generated := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *188  exact linearSpan.eq_of_submodule with source, target, hom, generated189190theorem linearSpan.subset_adjoin (G : Set)191  requires bounded : G ⊆ S192  shows linearSpan(f, R, S, G) ⊆ algebraAdjoin(f, R, S, G)193proof194  have generated := algebraAdjoin.subalgebra with source, target, hom, bounded195  have submodule := Subalgebra.submodule with source, target, hom, generated196  have generators := algebraAdjoin.contains with source, target, hom, bounded197  exact linearSpan.least with source, target, hom, submodule, generators198199theorem FiniteAlgebraModule.finitely_generated_algebra200  requires finiteModule : FiniteAlgebraModule(f, R, S)201  shows FinitelyGeneratedAlgebra(f, R, S)202proof203  obtain ⟨G, finite, bounded, spans⟩ := finiteModule204  have included := linearSpan.subset_adjoin with source, target, hom, bounded205  rw spans at included206  have subset := algebraAdjoin.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *207  have generated := Subset.antisymmetric with subset, included208  unfold FinitelyGeneratedAlgebra209  refine ⟨G, finite, bounded, generated⟩210211end Algebras212