DivisionBlock.lean

1 import KomorebiVerification.SemisimpleCompletion
2 import KomorebiVerification.SeedRankBasics
3 import KomorebiVerification.SeedRankOperations
4 import PaperICompletion8.DivisionRows
5 import KomorebiVerification.FullMatrixCyclicity
6 
7 /-! Canonical seed ranks for the actual left matrix module over a division ring. -/
8 set_option autoImplicit false
9 
10 -- Keep theorem bodies stable in this audit release while making the build warning-fatal.
11 set_option linter.unnecessarySimpa false
12 set_option linter.style.haveILetI false
13 set_option linter.unusedSectionVars false
14 
15 namespace Komorebi.PaperICompletion8.DivisionBlock
16 
17 open scoped BigOperators
18 
19 open Komorebi.SeedRankBasics
20 open Komorebi.SeedRankOperations
21 open Komorebi.PaperICompletion8.DivisionRows
22 
23 universe u v
24 
25 variable {k : Type u} [DivisionRing k]
26 
27 abbrev BlockAlgebra (d : ℕ) := Matrix (Fin d) (Fin d) k
28 
29 abbrev BlockModule (d m : ℕ) := Matrix (Fin d) (Fin m) k
30 
31 section BlockModules
32 
33 local instance (priority := 100) blockModuleAction (d m : ℕ) :
34     Module (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) :=
35   Matrix.Module.matrixModule
36 
37 /-- The scoped matrix-module action is ordinary multiplication on a
38 rectangular matrix. -/
39 theorem block_smul_eq_mul {d m : ℕ}
40     (A : BlockAlgebra (k := k) d) (V : BlockModule (k := k) d m) :
41     A • V = A * V := by
42   ext i j
43   change (∑ b, A i b • V b) j = ∑ b, A i b * V b j
44   simp
45 
46 /-- The bespoke row-space notion is exactly `FamilyGenerates` for the
47 canonical full-matrix module. -/
48 theorem leftGenerates_iff_familyGenerates {r d m : ℕ}
49     (v : Fin r → BlockModule (k := k) d m) :
50     LeftGenerates v ↔
51       FamilyGenerates (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) v := by
52   classical
53   rw [FamilyGenerates, Generates, eq_top_iff,
54     Submodule.top_le_span_range_iff_forall_exists_fun]
55   constructor
56   · intro h X
57     obtain ⟨A, hA⟩ := h X
58     refine ⟨A, ?_⟩
59     simpa only [block_smul_eq_mul] using hA.symm
60   · intro h X
61     obtain ⟨A, hA⟩ := h X
62     refine ⟨A, ?_⟩
63     simpa only [block_smul_eq_mul] using hA.symm
64 
65 open Komorebi.SemisimpleCompletion (seedFinrank_eq_of_exists_fin_family_iff)
66 
67 /-- The one-block ceiling count is the general `SeedRankBasics.seedFinrank`,
68 not merely a bespoke minimum. -/
69 theorem oneBlock_seedFinrank_eq_ceilDiv {d m : ℕ} (hd : 0 < d) :
70     seedFinrank (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) =
71       m ⌈/⌉ d := by
72   apply seedFinrank_eq_of_exists_fin_family_iff (c := m ⌈/⌉ d)
73   intro r
74   constructor
75   · rintro ⟨v, hv⟩
76     have hm : m ≤ r * d := (exists_leftGenerators_iff (k := k) hd).mp
77       ⟨v, (leftGenerates_iff_familyGenerates v).mpr hv⟩
78     apply (ceilDiv_le_iff_le_mul hd).mpr
79     simpa [Nat.mul_comm] using hm
80   · intro hr
81     have hm : m ≤ r * d := by
82       simpa [Nat.mul_comm] using (ceilDiv_le_iff_le_mul hd).mp hr
83     obtain ⟨v, hv⟩ := (exists_leftGenerators_iff (k := k) hd).mpr hm
84     exact ⟨v, (leftGenerates_iff_familyGenerates v).mp hv⟩
85 
86 /-- Cardinal-valued form of the same one-block formula. -/
87 theorem oneBlock_seedRank_eq_ceilDiv {d m : ℕ} (hd : 0 < d) :
88     seedRank (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) =
89       ((m ⌈/⌉ d : ℕ) : Cardinal) := by
90   classical
91   have hfin : Module.Finite (BlockAlgebra (k := k) d)
92       (BlockModule (k := k) d m) := by
93     obtain ⟨v, hv⟩ := exists_leftGenerators_of_le (k := k)
94       (r := m ⌈/⌉ d) hd (by
95         have hm : m ≤ d * (m ⌈/⌉ d) := (ceilDiv_le_iff_le_mul hd).mp le_rfl
96         simpa [Nat.mul_comm] using hm)
97     exact Module.Finite.of_surjective
98       (multiSeedMap (BlockAlgebra (k := k) d) (BlockModule (k := k) d m) v)
99       ((familyGenerates_iff_surjective _ _ v).mp
100         ((leftGenerates_iff_familyGenerates v).mp hv))
101   letI := hfin
102   rw [seedRank_eq_seedFinrank,
103     oneBlock_seedFinrank_eq_ceilDiv (k := k) hd]
104 
105 end BlockModules
106 
107 end Komorebi.PaperICompletion8.DivisionBlock

Back to source controls