SeedRankBasics.lean

1 import KomorebiVerification.MathlibImports
2 
3 /-!
4 # Algebraic seed-rank basics
5 
6 This file formalizes the algebraic foundation of Paper I.  A set of seeds
7 generates a module when its submodule span is the whole module.  The seed rank
8 is the least cardinality of such a set; this is Mathlib's `Submodule.spanRank`
9 applied to the top submodule, so the zero module and infinitely generated
10 modules are covered without extra conventions.
11 
12 For one seed, the presentation map is `a ↦ a • x`.  For a family of seeds,
13 it is the finite-linear-combination map from the free module `ι →₀ A`.
14 The first isomorphism theorem then gives the corresponding quotient
15 presentations.  We also prove monotonicity under surjective linear maps and
16 invariance under linear equivalence.
17 -/
18 
19 set_option autoImplicit false
20 
21 namespace Komorebi.SeedRankBasics
22 
23 open Cardinal Set
24 
25 universe u v w
26 
27 section Semiring
28 
29 variable (A : Type u) (M : Type v)
30 variable [Semiring A] [AddCommMonoid M] [Module A M]
31 
32 /-- A set of seeds generates `M` when its `A`-linear span is all of `M`. -/
33 def Generates (s : Set M) : Prop :=
34   Submodule.span A s = ⊤
35 
36 /-- A family generates when its range is a generating set. -/
37 def FamilyGenerates {ι : Type w} (v : ι → M) : Prop :=
38   Generates A M (Set.range v)
39 
40 /-- A module is cyclic when one element generates it. -/
41 def Cyclic : Prop :=
42   ∃ x : M, Generates A M {x}
43 
44 /--
45 The seed rank is the least cardinality of a set whose `A`-span is `M`.
46 
47 Because it is cardinal-valued, it remains meaningful for modules that are not
48 finitely generated.  In particular, the zero module has seed rank zero.
49 -/
50 noncomputable def seedRank : Cardinal :=
51   (⊤ : Submodule A M).spanRank
52 
53 /-- The natural-valued minimum used for finite-generation corollaries. -/
54 noncomputable def seedFinrank : ℕ :=
55   (⊤ : Submodule A M).spanFinrank
56 
57 theorem generates_univ : Generates A M Set.univ := by
58   simp [Generates]
59 
60 theorem generates_mono {s t : Set M} (hs : Generates A M s) (hst : s ⊆ t) :
61     Generates A M t := by
62   rw [Generates] at hs ⊢
63   exact top_unique (hs ▸ Submodule.span_mono hst)
64 
65 /-- Every generating set gives an upper bound for seed rank. -/
66 theorem seedRank_le_mk_of_generates {s : Set M} (hs : Generates A M s) :
67     seedRank A M ≤ Cardinal.mk s := by
68   rw [Generates] at hs
69   rw [seedRank, ← hs]
70   exact Submodule.spanRank_span_le_card s
71 
72 /-- A minimum-cardinality generating set always exists. -/
73 theorem exists_generating_set_card_eq_seedRank :
74     ∃ s : Set M, Generates A M s ∧ Cardinal.mk s = seedRank A M := by
75   obtain ⟨s, hsCard, hsSpan⟩ :=
76     Submodule.exists_span_set_card_eq_spanRank (⊤ : Submodule A M)
77   exact ⟨s, hsSpan, hsCard⟩
78 
79 /-- The universal one-seed presentation map, `a ↦ a • x`. -/
80 def oneSeedMap (x : M) : A →ₗ[A] M :=
81   LinearMap.toSpanSingleton A M x
82 
83 @[simp]
84 theorem oneSeedMap_apply (x : M) (a : A) :
85     oneSeedMap A M x a = a • x := by
86   rfl
87 
88 /-- The image of the one-seed map is exactly the cyclic submodule it spans. -/
89 theorem range_oneSeedMap (x : M) :
90     LinearMap.range (oneSeedMap A M x) = Submodule.span A {x} := by
91   exact LinearMap.range_toSpanSingleton x
92 
93 /-- A seed generates exactly when its presentation map is surjective. -/
94 theorem generates_singleton_iff_surjective (x : M) :
95     Generates A M {x} ↔ Function.Surjective (oneSeedMap A M x) := by
96   rw [Generates, ← range_oneSeedMap A M x, LinearMap.range_eq_top]
97 
98 /-- Cyclicity is equivalently the existence of a surjective one-seed map. -/
99 theorem cyclic_iff_exists_surjective_oneSeedMap :
100     Cyclic A M ↔
101       ∃ x : M, Function.Surjective (oneSeedMap A M x) := by
102   simp only [Cyclic, generates_singleton_iff_surjective]
103 
104 /-- The multi-seed presentation map from the free module on the seed labels. -/
105 noncomputable def multiSeedMap {ι : Type w} (v : ι → M) : (ι →₀ A) →ₗ[A] M :=
106   Finsupp.linearCombination A v
107 
108 /-- Its image is exactly the span of the seed family. -/
109 theorem range_multiSeedMap {ι : Type w} (v : ι → M) :
110     LinearMap.range (multiSeedMap A M v) =
111       Submodule.span A (Set.range v) := by
112   exact Finsupp.range_linearCombination (R := A) (v := v)
113 
114 /-- A family generates exactly when its free-module presentation is onto. -/
115 theorem familyGenerates_iff_surjective {ι : Type w} (v : ι → M) :
116     FamilyGenerates A M v ↔
117       Function.Surjective (multiSeedMap A M v) := by
118   rw [FamilyGenerates, Generates, ← range_multiSeedMap A M v,
119     LinearMap.range_eq_top]
120 
121 /-- A generating family bounds seed rank by the cardinality of its labels. -/
122 theorem seedRank_le_mk_of_familyGenerates {ι : Type w} {v : ι → M}
123     (hv : FamilyGenerates A M v) :
124     Cardinal.lift.{w} (seedRank A M) ≤ Cardinal.lift.{v} (Cardinal.mk ι) := by
125   have hset := seedRank_le_mk_of_generates A M hv
126   exact (Cardinal.lift_le.2 hset).trans
127     (Cardinal.mk_range_le_lift (f := v))
128 
129 /-- Seed rank zero characterizes the zero (subsingleton) module. -/
130 theorem seedRank_eq_zero_iff :
131     seedRank A M = 0 ↔ Subsingleton M := by
132   rw [seedRank, Submodule.spanRank_eq_zero_iff_eq_bot]
133   constructor
134   · intro h
135     constructor
136     intro x y
137     have hx : x = 0 := by
138       have hx' : x ∈ (⊥ : Submodule A M) := by
139         rw [← h]
140         trivial
141       simpa using hx'
142     have hy : y = 0 := by
143       have hy' : y ∈ (⊥ : Submodule A M) := by
144         rw [← h]
145         trivial
146       simpa using hy'
147     exact hx.trans hy.symm
148   · intro h
149     apply le_antisymm
150     · intro x _hx
151       change x = 0
152       exact @Subsingleton.elim M h x 0
153     · exact bot_le
154 
155 /-- Seed rank is below `aleph0` exactly when the module is finitely generated. -/
156 theorem seedRank_lt_aleph0_iff :
157     seedRank A M < Cardinal.aleph0 ↔ Module.Finite A M := by
158   rw [seedRank, Submodule.spanRank_finite_iff_fg]
159   exact Module.finite_def.symm
160 
161 /-- Cyclicity is the principality of the top submodule. -/
162 theorem cyclic_iff_top_isPrincipal :
163     Cyclic A M ↔ (⊤ : Submodule A M).IsPrincipal := by
164   constructor
165   · rintro ⟨x, hx⟩
166     exact ⟨x, hx.symm⟩
167   · rintro ⟨x, hx⟩
168     exact ⟨x, hx.symm⟩
169 
170 /-- In a finite module, cardinal seed rank is the natural seed finrank. -/
171 theorem seedRank_eq_seedFinrank [Module.Finite A M] :
172     seedRank A M = seedFinrank A M := by
173   exact Module.Finite.fg_top.spanRank_eq_spanFinrank
174 
175 /-- Finite, nonzero cyclic modules are exactly those of seed finrank one. -/
176 theorem cyclic_iff_seedFinrank_eq_one [Module.Finite A M] [Nontrivial M] :
177     Cyclic A M ↔ seedFinrank A M = 1 := by
178   rw [seedFinrank, Submodule.spanFinrank_eq_one_iff]
179   simpa using cyclic_iff_top_isPrincipal A M
180 
181 /-- For a finite nonzero module, cardinal seed rank one is exactly cyclicity. -/
182 theorem seedRank_eq_one_iff_cyclic [Module.Finite A M] [Nontrivial M] :
183     seedRank A M = 1 ↔ Cyclic A M := by
184   rw [seedRank_eq_seedFinrank A M]
185   norm_cast
186   exact (cyclic_iff_seedFinrank_eq_one A M).symm
187 
188 end Semiring
189 
190 section Functoriality
191 
192 variable {A : Type u} {M N : Type v}
193 variable [Semiring A]
194 variable [AddCommMonoid M] [Module A M]
195 variable [AddCommMonoid N] [Module A N]
196 
197 /-- Seed rank cannot increase under a surjective linear map. -/
198 theorem seedRank_le_of_surjective (f : M →ₗ[A] N)
199     (hf : Function.Surjective f) :
200     seedRank A N ≤ seedRank A M := by
201   rw [seedRank, seedRank, ← LinearMap.range_eq_top.mpr hf]
202   exact Submodule.spanRank_range_le f
203 
204 /-- Seed rank is invariant under linear equivalence. -/
205 theorem seedRank_linearEquiv (e : M ≃ₗ[A] N) :
206     seedRank A M = seedRank A N := by
207   apply le_antisymm
208   · exact seedRank_le_of_surjective e.symm.toLinearMap e.symm.surjective
209   · exact seedRank_le_of_surjective e.toLinearMap e.surjective
210 
211 end Functoriality
212 
213 section QuotientPresentations
214 
215 variable (A : Type u) (M : Type v)
216 variable [Ring A] [AddCommGroup M] [Module A M]
217 
218 /-- Passing to a module quotient cannot increase seed rank. -/
219 theorem seedRank_quotient_le (p : Submodule A M) :
220     seedRank A (M ⧸ p) ≤ seedRank A M := by
221   exact seedRank_le_of_surjective p.mkQ p.mkQ_surjective
222 
223 /-- First-isomorphism presentation for one seed, with its exact range. -/
224 noncomputable def oneSeedQuotientEquivRange (x : M) :
225     (A ⧸ LinearMap.ker (oneSeedMap A M x)) ≃ₗ[A]
226       LinearMap.range (oneSeedMap A M x) :=
227   (oneSeedMap A M x).quotKerEquivRange
228 
229 /--
230 The range-valued quotient equivalence is the canonical presentation map:
231 the class of `a` is sent to the range element represented by `a • x`.
232 This is the explicit glue between the first-isomorphism construction and the
233 formula used in the manuscript.
234 -/
235 @[simp]
236 theorem oneSeedQuotientEquivRange_apply_mk (x : M) (a : A) :
237     (oneSeedQuotientEquivRange A M x) (Submodule.Quotient.mk a) =
238       ⟨a • x, by
239         exact ⟨a, rfl⟩⟩ := by
240   rfl
241 
242 /-- If `x` generates, its quotient presentation has codomain all of `M`. -/
243 noncomputable def oneSeedQuotientEquiv (x : M)
244     (hx : Generates A M {x}) :
245     (A ⧸ LinearMap.ker (oneSeedMap A M x)) ≃ₗ[A] M :=
246   (oneSeedMap A M x).quotKerEquivOfSurjective
247     ((generates_singleton_iff_surjective A M x).mp hx)
248 
249 @[simp]
250 theorem oneSeedQuotientEquiv_apply_mk (x : M)
251     (hx : Generates A M {x}) (a : A) :
252     oneSeedQuotientEquiv A M x hx (Submodule.Quotient.mk a) = a • x := by
253   rfl
254 
255 /-- First-isomorphism presentation for an arbitrary seed family. -/
256 noncomputable def multiSeedQuotientEquivRange {ι : Type w} (v : ι → M) :
257     ((ι →₀ A) ⧸ LinearMap.ker (multiSeedMap A M v)) ≃ₗ[A]
258       LinearMap.range (multiSeedMap A M v) :=
259   (multiSeedMap A M v).quotKerEquivRange
260 
261 /--
262 The range-valued multi-seed quotient equivalence sends a coefficient family
263 to its represented finite linear combination.  This makes the free-module
264 presentation in the manuscript literal at the level of the compiled API.
265 -/
266 @[simp]
267 theorem multiSeedQuotientEquivRange_apply_mk {ι : Type w} (v : ι → M)
268     (c : ι →₀ A) :
269     (multiSeedQuotientEquivRange A M v) (Submodule.Quotient.mk c) =
270       ⟨Finsupp.linearCombination A v c, by
271         exact ⟨c, rfl⟩⟩ := by
272   rfl
273 
274 /-- A generating family presents `M` as a quotient of its free module. -/
275 noncomputable def multiSeedQuotientEquiv {ι : Type w} (v : ι → M)
276     (hv : FamilyGenerates A M v) :
277     ((ι →₀ A) ⧸ LinearMap.ker (multiSeedMap A M v)) ≃ₗ[A] M :=
278   (multiSeedMap A M v).quotKerEquivOfSurjective
279     ((familyGenerates_iff_surjective A M v).mp hv)
280 
281 @[simp]
282 theorem multiSeedQuotientEquiv_apply_mk {ι : Type w} (v : ι → M)
283     (hv : FamilyGenerates A M v) (c : ι →₀ A) :
284     multiSeedQuotientEquiv A M v hv (Submodule.Quotient.mk c) =
285       Finsupp.linearCombination A v c := by
286   rfl
287 
288 end QuotientPresentations
289 
290 end Komorebi.SeedRankBasics
291 
292 #print axioms Komorebi.SeedRankBasics.seedRank_le_of_surjective
293 #print axioms Komorebi.SeedRankBasics.seedRank_linearEquiv
294 #print axioms Komorebi.SeedRankBasics.oneSeedQuotientEquiv
295 #print axioms Komorebi.SeedRankBasics.multiSeedQuotientEquiv
296 #print axioms Komorebi.SeedRankBasics.cyclic_iff_seedFinrank_eq_one

Back to source controls