SemisimpleCompletion.lean

1 import KomorebiVerification.SeedRankBasics
2 import KomorebiVerification.SeedRankOperations
3 import KomorebiVerification.SemisimpleSeedRank
4 import KomorebiVerification.FullMatrixCyclicity
5 
6 /-!
7 # Completion bridges for the semisimple claims in Paper I
8 
9 This file connects the row-space generator count proved in
10 `SemisimpleSeedRank` to the general `SeedRankBasics` invariant.  It then
11 assembles finitely many split simple blocks in the literal product algebra
12 
13 `∀ i, Matrix (Fin (d i)) (Fin (d i)) k`
14 
15 acting coordinatewise on the literal product module
16 
17 `∀ i, Matrix (Fin (d i)) (Fin (m i)) k`.
18 
19 Thus the assembly theorem assumes the displayed Wedderburn decomposition as
20 data: it does not formalize or invoke a classification theorem.  The final
21 corollaries are literal bridges to the full-matrix cyclicity and multiplicity
22 obstruction statements in Paper I.
23 -/
24 
25 set_option autoImplicit false
26 
27 -- Keep theorem bodies stable in this audit release while making the build warning-fatal.
28 set_option linter.unnecessarySimpa false
29 set_option linter.style.haveILetI false
30 set_option linter.unusedSectionVars false
31 
32 namespace Komorebi.SemisimpleCompletion
33 
34 open scoped BigOperators
35 
36 open Komorebi.SeedRankBasics
37 open Komorebi.SeedRankOperations
38 open Komorebi.SemisimpleSeedRank
39 
40 universe u v
41 
42 variable {k : Type u} [Field k]
43 
44 abbrev BlockAlgebra (d : ℕ) := Matrix (Fin d) (Fin d) k
45 
46 abbrev BlockModule (d m : ℕ) := Matrix (Fin d) (Fin m) k
47 
48 section BlockModules
49 
50 local instance (priority := 100) blockModuleAction (d m : ℕ) :
51     Module (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) :=
52   Matrix.Module.matrixModule
53 
54 /-- The scoped matrix-module action is ordinary multiplication on a
55 rectangular matrix. -/
56 theorem block_smul_eq_mul {d m : ℕ}
57     (A : BlockAlgebra (k := k) d) (V : BlockModule (k := k) d m) :
58     A • V = A * V := by
59   ext i j
60   change (∑ b, A i b • V b) j = ∑ b, A i b * V b j
61   simp
62 
63 /-- The bespoke row-space notion is exactly `FamilyGenerates` for the
64 canonical full-matrix module. -/
65 theorem leftGenerates_iff_familyGenerates {r d m : ℕ}
66     (v : Fin r → BlockModule (k := k) d m) :
67     LeftGenerates v ↔
68       FamilyGenerates (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) v := by
69   classical
70   rw [FamilyGenerates, Generates, eq_top_iff,
71     Submodule.top_le_span_range_iff_forall_exists_fun]
72   constructor
73   · intro h X
74     obtain ⟨A, hA⟩ := h X
75     refine ⟨A, ?_⟩
76     simpa only [block_smul_eq_mul] using hA.symm
77   · intro h X
78     obtain ⟨A, hA⟩ := h X
79     refine ⟨A, ?_⟩
80     simpa only [block_smul_eq_mul] using hA.symm
81 
82 /-- A reusable minimum principle: if `c ≤ r` exactly characterizes the
83 existence of a generating `Fin r`-family, then the general natural-valued
84 seed rank is `c`.  The existence direction supplies finite generation, so no
85 separate finiteness hypothesis is hidden here. -/
86 theorem seedFinrank_eq_of_exists_fin_family_iff
87     {A : Type u} {M : Type v}
88     [Semiring A] [AddCommMonoid M] [Module A M]
89     (c : ℕ)
90     (hcount : ∀ r : ℕ,
91       (∃ v : Fin r → M, FamilyGenerates A M v) ↔ c ≤ r) :
92     seedFinrank A M = c := by
93   classical
94   obtain ⟨v, hv⟩ := (hcount c).mpr le_rfl
95   letI : Module.Finite A M :=
96     Module.Finite.of_surjective (multiSeedMap A M v)
97       ((familyGenerates_iff_surjective A M v).mp hv)
98   apply le_antisymm
99   · rw [seedFinrank, ← hv]
100     refine (Submodule.spanFinrank_span_le_ncard_of_finite
101       (Set.finite_range v)).trans ?_
102     rw [← Set.image_univ]
103     simpa using Set.ncard_image_le (f := v) (s := Set.univ)
104   · obtain ⟨s, hsCard, hsSpan⟩ :=
105       Module.Finite.fg_top.exists_span_finset_card_eq_spanFinrank
106         (R := A) (M := M)
107     let e : Fin s.card ≃ {x : M // x ∈ s} := by
108       simpa using (Fintype.equivFin {x : M // x ∈ s}).symm
109     let w : Fin s.card → M := fun j ↦ (e j : M)
110     have hwRange : Set.range w = (s : Set M) := by
111       ext x
112       constructor
113       · rintro ⟨j, rfl⟩
114         exact (e j).property
115       · intro hx
116         let y : {x : M // x ∈ s} := ⟨x, hx⟩
117         refine ⟨e.symm y, ?_⟩
118         simp [w, y]
119     have hw : FamilyGenerates A M w := by
120       rw [FamilyGenerates, Generates, hwRange, hsSpan]
121     have hc : c ≤ s.card := (hcount s.card).mp ⟨w, hw⟩
122     simpa [seedFinrank, hsCard] using hc
123 
124 /-- The one-block ceiling count is the general `SeedRankBasics.seedFinrank`,
125 not merely a bespoke minimum. -/
126 theorem oneBlock_seedFinrank_eq_ceilDiv {d m : ℕ} (hd : 0 < d) :
127     seedFinrank (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) =
128       m ⌈/⌉ d := by
129   apply seedFinrank_eq_of_exists_fin_family_iff (c := m ⌈/⌉ d)
130   intro r
131   constructor
132   · rintro ⟨v, hv⟩
133     have hm : m ≤ r * d := (exists_leftGenerators_iff (k := k) hd).mp
134       ⟨v, (leftGenerates_iff_familyGenerates v).mpr hv⟩
135     apply (ceilDiv_le_iff_le_mul hd).mpr
136     simpa [Nat.mul_comm] using hm
137   · intro hr
138     have hm : m ≤ r * d := by
139       simpa [Nat.mul_comm] using (ceilDiv_le_iff_le_mul hd).mp hr
140     obtain ⟨v, hv⟩ := (exists_leftGenerators_iff (k := k) hd).mpr hm
141     exact ⟨v, (leftGenerates_iff_familyGenerates v).mp hv⟩
142 
143 /-- Cardinal-valued form of the same one-block formula. -/
144 theorem oneBlock_seedRank_eq_ceilDiv {d m : ℕ} (hd : 0 < d) :
145     seedRank (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) =
146       ((m ⌈/⌉ d : ℕ) : Cardinal) := by
147   classical
148   have hfin : Module.Finite (BlockAlgebra (k := k) d)
149       (BlockModule (k := k) d m) := by
150     obtain ⟨v, hv⟩ := exists_leftGenerators_of_le (k := k)
151       (r := m ⌈/⌉ d) hd (by
152         have hm : m ≤ d * (m ⌈/⌉ d) := (ceilDiv_le_iff_le_mul hd).mp le_rfl
153         simpa [Nat.mul_comm] using hm)
154     exact Module.Finite.of_surjective
155       (multiSeedMap (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) v)
156       ((familyGenerates_iff_surjective _ _ v).mp
157         ((leftGenerates_iff_familyGenerates v).mp hv))
158   letI := hfin
159   rw [seedRank_eq_seedFinrank,
160     oneBlock_seedFinrank_eq_ceilDiv (k := k) hd]
161 
162 section FiniteProduct
163 
164 variable {I : Type v} [Fintype I] [DecidableEq I]
165 variable (d m : I → ℕ)
166 
167 /-- The literal finite product algebra in the split Wedderburn hypothesis. -/
168 abbrev SplitProductAlgebra :=
169   ∀ i : I, BlockAlgebra (k := k) (d i)
170 
171 /-- The literal product of the corresponding isotypic matrix modules. -/
172 abbrev SplitProductModule :=
173   ∀ i : I, BlockModule (k := k) (d i) (m i)
174 
175 /-- The maximum of the blockwise ceiling requirements.  `Finset.sup` gives
176 value zero for an empty product; Paper I assumes a nonempty block set. -/
177 def maxCeilDiv : ℕ :=
178   Finset.univ.sup (fun i : I ↦ m i ⌈/⌉ d i)
179 
180 /-- A family generates the literal product module exactly when its projection
181 to every isotypic block generates that block.  The proof assembles the
182 blockwise coefficient matrices into elements of the product algebra. -/
183 theorem splitProduct_familyGenerates_iff {r : ℕ}
184     (v : Fin r → SplitProductModule (k := k) d m) :
185     FamilyGenerates (SplitProductAlgebra (k := k) d)
186         (SplitProductModule (k := k) d m) v ↔
187       ∀ i : I, LeftGenerates (fun j ↦ v j i) := by
188   classical
189   rw [FamilyGenerates, Generates, eq_top_iff,
190     Submodule.top_le_span_range_iff_forall_exists_fun]
191   constructor
192   · intro h i X
193     obtain ⟨c, hc⟩ := h (Pi.single i X)
194     refine ⟨fun j ↦ c j i, ?_⟩
195     calc
196       X = (Pi.single i X : SplitProductModule (k := k) d m) i := by simp
197       _ = (∑ j, c j • v j) i := by rw [hc]
198       _ = ∑ j, (c j i) * (v j i) := by
199         simp only [Finset.sum_apply, Pi.smul_apply', block_smul_eq_mul]
200   · intro h X
201     choose c hc using fun i ↦ h i (X i)
202     let a : Fin r → SplitProductAlgebra (k := k) d :=
203       fun j i ↦ c i j
204     refine ⟨a, ?_⟩
205     funext i
206     simpa only [Finset.sum_apply, Pi.smul_apply', block_smul_eq_mul, a]
207       using (hc i).symm
208 
209 /-- Existence of `r` product generators is equivalent to the simultaneous
210 row-dimension inequalities on all simple blocks. -/
211 theorem exists_splitProduct_generators_iff_coordinate_bounds
212     {r : ℕ} (hd : ∀ i, 0 < d i) :
213     (∃ v : Fin r → SplitProductModule (k := k) d m,
214       FamilyGenerates (SplitProductAlgebra (k := k) d)
215         (SplitProductModule (k := k) d m) v) ↔
216       ∀ i : I, m i ≤ r * d i := by
217   constructor
218   · rintro ⟨v, hv⟩ i
219     exact multiplicity_le_of_leftGenerates (k := k) (hd i)
220       ((splitProduct_familyGenerates_iff d m v).mp hv i)
221   · intro h
222     choose w hw using fun i ↦
223       exists_leftGenerators_of_le (k := k) (hd i) (h i)
224     let v : Fin r → SplitProductModule (k := k) d m :=
225       fun j i ↦ w i j
226     refine ⟨v, (splitProduct_familyGenerates_iff d m v).mpr ?_⟩
227     intro i
228     simpa only [v] using hw i
229 
230 /-- The finite-product assembly criterion: `r` seeds exist exactly when `r`
231 is at least the maximum blockwise ceiling. -/
232 theorem exists_splitProduct_generators_iff_maxCeilDiv_le
233     {r : ℕ} (hd : ∀ i, 0 < d i) :
234     (∃ v : Fin r → SplitProductModule (k := k) d m,
235       FamilyGenerates (SplitProductAlgebra (k := k) d)
236         (SplitProductModule (k := k) d m) v) ↔
237       maxCeilDiv d m ≤ r := by
238   rw [exists_splitProduct_generators_iff_coordinate_bounds d m hd]
239   constructor
240   · intro h
241     apply Finset.sup_le
242     intro i hi
243     apply (ceilDiv_le_iff_le_mul (hd i)).mpr
244     simpa [Nat.mul_comm] using h i
245   · intro h i
246     have hblock : m i ⌈/⌉ d i ≤ maxCeilDiv d m :=
247       Finset.le_sup (f := fun j : I ↦ m j ⌈/⌉ d j) (Finset.mem_univ i)
248     have hceil : m i ⌈/⌉ d i ≤ r := hblock.trans h
249     have hm : m i ≤ d i * r := (ceilDiv_le_iff_le_mul (hd i)).mp hceil
250     simpa [Nat.mul_comm] using hm
251 
252 /-- The displayed maximum is the least possible size of a finite generating
253 family for the split product module. -/
254 theorem maxCeilDiv_isLeast_product_generatorCount
255     (hd : ∀ i, 0 < d i) :
256     IsLeast
257       {r : ℕ |
258         ∃ v : Fin r → SplitProductModule (k := k) d m,
259           FamilyGenerates (SplitProductAlgebra (k := k) d)
260             (SplitProductModule (k := k) d m) v}
261       (maxCeilDiv d m) := by
262   constructor
263   · exact (exists_splitProduct_generators_iff_maxCeilDiv_le
264       (k := k) d m hd).mpr le_rfl
265   · intro r hr
266     exact (exists_splitProduct_generators_iff_maxCeilDiv_le
267       (k := k) d m hd).mp hr
268 
269 /-- Paper I's finite split-semisimple multiplicity formula for the literal
270 decomposition displayed above. -/
271 theorem splitProduct_seedFinrank_eq_maxCeilDiv
272     (hd : ∀ i, 0 < d i) :
273     seedFinrank (SplitProductAlgebra (k := k) d)
274         (SplitProductModule (k := k) d m) =
275       maxCeilDiv d m := by
276   apply seedFinrank_eq_of_exists_fin_family_iff
277   intro r
278   exact exists_splitProduct_generators_iff_maxCeilDiv_le (k := k) d m hd
279 
280 /-- Cardinal-valued form of the finite split-semisimple multiplicity
281 formula. -/
282 theorem splitProduct_seedRank_eq_maxCeilDiv
283     (hd : ∀ i, 0 < d i) :
284     seedRank (SplitProductAlgebra (k := k) d)
285         (SplitProductModule (k := k) d m) =
286       ((maxCeilDiv d m : ℕ) : Cardinal) := by
287   classical
288   obtain ⟨v, hv⟩ :=
289     (exists_splitProduct_generators_iff_maxCeilDiv_le (k := k) d m hd).mpr le_rfl
290   letI : Module.Finite (SplitProductAlgebra (k := k) d)
291       (SplitProductModule (k := k) d m) :=
292     Module.Finite.of_surjective
293       (multiSeedMap (SplitProductAlgebra (k := k) d)
294         (SplitProductModule (k := k) d m) v)
295       ((familyGenerates_iff_surjective _ _ v).mp hv)
296   rw [seedRank_eq_seedFinrank,
297     splitProduct_seedFinrank_eq_maxCeilDiv d m hd]
298 
299 /-- Transport of the formula to any module supplied with an explicit linear
300 decomposition over the literal product algebra.  This is the exact hypothesis
301 needed after transporting an abstract split semisimple algebra along a chosen
302 Wedderburn isomorphism. -/
303 theorem seedRank_eq_maxCeilDiv_of_splitProduct_decomposition
304     {X : Type (max u v)} [AddCommMonoid X]
305     [Module (SplitProductAlgebra (k := k) d) X]
306     (e : X ≃ₗ[SplitProductAlgebra (k := k) d]
307       SplitProductModule (k := k) d m)
308     (hd : ∀ i, 0 < d i) :
309     seedRank (SplitProductAlgebra (k := k) d) X =
310       ((maxCeilDiv d m : ℕ) : Cardinal) := by
311   rw [seedRank_linearEquiv e,
312     splitProduct_seedRank_eq_maxCeilDiv d m hd]
313 
314 end FiniteProduct
315 
316 end BlockModules
317 
318 section AbstractSplitDecomposition
319 
320 variable {I : Type u} [Fintype I] [DecidableEq I]
321 variable (d m : I → ℕ)
322 
323 attribute [local instance] RingHomInvPair.of_ringEquiv
324 
325 local instance abstractSplitBlockModuleAction (i : I) :
326     Module (BlockAlgebra (k := k) (d i))
327       (BlockModule (k := k) (d i) (m i)) :=
328   Matrix.Module.matrixModule
329 
330 /--
331 Exact transport form of Paper I's split-semisimple hypothesis.
332 
333 The hypotheses supply, rather than derive:
334 
335 * a chosen `k`-algebra isomorphism from the abstract acting algebra `A` to
336   the finite product of full matrix algebras; and
337 * a chosen semilinear equivalence from `X` to the corresponding product of
338   isotypic matrix modules, whose scalar law is precisely that algebra
339   isomorphism.
340 
341 No existence or classification part of Wedderburn--Artin is asserted here.
342 -/
343 theorem semisimple_seedRank_eq_maxCeilDiv_of_equivalences
344     {A X : Type u} [Semiring A] [Algebra k A]
345     [AddCommMonoid X] [Module A X]
346     (algebraEquiv : A ≃ₐ[k] SplitProductAlgebra (k := k) d)
347     (moduleEquiv : X ≃ₛₗ[RingHomClass.toRingHom algebraEquiv.toRingEquiv]
348       SplitProductModule (k := k) d m)
349     (hd : ∀ i, 0 < d i) :
350     seedRank A X = ((maxCeilDiv d m : ℕ) : Cardinal) := by
351   letI : RingHomSurjective
352       (RingHomClass.toRingHom algebraEquiv.toRingEquiv) :=
353     ⟨algebraEquiv.surjective⟩
354   calc
355     seedRank A X =
356         seedRank (SplitProductAlgebra (k := k) d)
357           (SplitProductModule (k := k) d m) :=
358       seedRank_eq_of_bijective_semilinear moduleEquiv.toLinearMap
359         moduleEquiv.bijective
360     _ = ((maxCeilDiv d m : ℕ) : Cardinal) :=
361       splitProduct_seedRank_eq_maxCeilDiv (k := k) d m hd
362 
363 end AbstractSplitDecomposition
364 
365 section FullMatrixCorollaries
366 
367 variable {n : ℕ}
368 
369 /-- `FullMatrixCyclicity.IsCyclic` is exactly singleton generation in the
370 general seed-rank module for the natural full-matrix action. -/
371 theorem fullMatrix_isCyclic_iff_generates (x : Fin n → k) :
372     Komorebi.FullMatrixCyclicity.IsCyclic x ↔
373       Generates (Matrix (Fin n) (Fin n) k) (Fin n → k) {x} := by
374   rw [generates_singleton_iff_surjective]
375   constructor
376   · intro hx y
377     obtain ⟨A, hA⟩ := hx y
378     refine ⟨A, ?_⟩
379     simpa [oneSeedMap_apply, Matrix.smul_eq_mulVec] using hA
380   · intro hx y
381     obtain ⟨A, hA⟩ := hx y
382     refine ⟨A, ?_⟩
383     simpa [oneSeedMap_apply, Matrix.smul_eq_mulVec] using hA
384 
385 /-- Literal Paper I statement: every nonzero coordinate vector generates the
386 natural module over the full matrix algebra. -/
387 theorem fullMatrix_every_nonzero_vector_generates
388     {x : Fin n → k} (hx : x ≠ 0) :
389     Generates (Matrix (Fin n) (Fin n) k) (Fin n → k) {x} :=
390   (fullMatrix_isCyclic_iff_generates x).mp
391     (Komorebi.FullMatrixCyclicity.isCyclic_of_ne_zero hx)
392 
393 /-- The nonzero natural full-matrix module is cyclic in the general
394 `SeedRankBasics` sense. -/
395 theorem fullMatrix_module_cyclic (hn : 0 < n) :
396     Cyclic (Matrix (Fin n) (Fin n) k) (Fin n → k) := by
397   let i₀ : Fin n := ⟨0, hn⟩
398   let x : Fin n → k := Pi.single i₀ 1
399   have hx : x ≠ 0 := by
400     intro hzero
401     have hentry := congrFun hzero i₀
402     simpa [x] using hentry
403   exact ⟨x, fullMatrix_every_nonzero_vector_generates hx⟩
404 
405 /-- Literal seed-rank corollary for the natural full-matrix module. -/
406 theorem fullMatrix_seedRank_eq_one (hn : 0 < n) :
407     seedRank (Matrix (Fin n) (Fin n) k) (Fin n → k) = 1 := by
408   classical
409   have hcyc := fullMatrix_module_cyclic (k := k) hn
410   obtain ⟨x, hx⟩ := hcyc
411   have hsurj : Function.Surjective
412       (oneSeedMap (Matrix (Fin n) (Fin n) k) (Fin n → k) x) :=
413     (generates_singleton_iff_surjective _ _ x).mp hx
414   letI : Module.Finite (Matrix (Fin n) (Fin n) k) (Fin n → k) :=
415     Module.Finite.of_surjective
416       (oneSeedMap (Matrix (Fin n) (Fin n) k) (Fin n → k) x) hsurj
417   letI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
418   exact (seedRank_eq_one_iff_cyclic
419     (Matrix (Fin n) (Fin n) k) (Fin n → k)).mpr ⟨x, hx⟩
420 
421 end FullMatrixCorollaries
422 
423 section MultiplicityCorollaries
424 
425 variable {r d m : ℕ}
426 
427 local instance multiplicityBlockModuleAction (d m : ℕ) :
428     Module (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) :=
429   Matrix.Module.matrixModule
430 
431 /-- Literal multiplicity obstruction in the general generation language:
432 any `r` seeds for `m` copies of the natural `d`-dimensional module force
433 `ceil(m/d) ≤ r`. -/
434 theorem multiplicity_obstruction
435     (hd : 0 < d) {v : Fin r → BlockModule (k := k) d m}
436     (hv : FamilyGenerates (BlockAlgebra (k := k) d)
437       (BlockModule (k := k) d m) v) :
438     m ⌈/⌉ d ≤ r := by
439   apply (ceilDiv_le_iff_le_mul hd).mpr
440   have hm : m ≤ r * d := multiplicity_le_of_leftGenerates (k := k) hd
441     ((leftGenerates_iff_familyGenerates v).mpr hv)
442   simpa [Nat.mul_comm] using hm
443 
444 /-- Literal Paper I formula for the diagonal action on `m` copies of the
445 natural `d`-dimensional module. -/
446 theorem multiplicity_seedRank_formula (hd : 0 < d) :
447     seedRank (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) =
448       ((m ⌈/⌉ d : ℕ) : Cardinal) :=
449   oneBlock_seedRank_eq_ceilDiv (k := k) hd
450 
451 end MultiplicityCorollaries
452 
453 end Komorebi.SemisimpleCompletion
454 
455 #print axioms Komorebi.SemisimpleCompletion.oneBlock_seedRank_eq_ceilDiv
456 #print axioms Komorebi.SemisimpleCompletion.splitProduct_seedRank_eq_maxCeilDiv
457 #print axioms Komorebi.SemisimpleCompletion.semisimple_seedRank_eq_maxCeilDiv_of_equivalences
458 #print axioms Komorebi.SemisimpleCompletion.fullMatrix_seedRank_eq_one
459 #print axioms Komorebi.SemisimpleCompletion.multiplicity_obstruction

Back to source controls