SemisimpleSeedRank.lean

1 import KomorebiVerification.MathlibImports
2 
3 /-!
4 # The one-block semisimple seed-rank formula
5 
6 Let `k` be a field.  We identify the direct sum of `m` copies of `k^d` with
7 `d`-by-`m` matrices.  The algebra `M_d(k)` acts diagonally, by multiplication
8 on the left.  This file proves that `r` such matrices can generate the whole
9 module exactly when `m ≤ r * d`.  Consequently the least possible number
10 of generators is the ceiling quotient `m ⌈/⌉ d` (for `0 < d`).
11 
12 The proof is elementary and does not appeal to a pre-existing seed-rank
13 formula.  Its key step identifies module generation with spanning the space
14 of row vectors by the `r * d` rows of the proposed generators.
15 -/
16 
17 set_option autoImplicit false
18 
19 namespace Komorebi.SemisimpleSeedRank
20 
21 open scoped BigOperators
22 
23 universe u
24 
25 variable {k : Type u} [Field k]
26 variable {r d m : ℕ}
27 
28 /--
29 `LeftGenerates v` says that the `r` matrices `v i` generate all `d`-by-`m`
30 matrices under the diagonal left action of `M_d(k)`.
31 -/
32 def LeftGenerates
33     (v : Fin r → Matrix (Fin d) (Fin m) k) : Prop :=
34   ∀ X : Matrix (Fin d) (Fin m) k,
35     ∃ A : Fin r → Matrix (Fin d) (Fin d) k,
36       X = ∑ i, A i * v i
37 
38 /-- The `r * d` rows of `v` span the row-vector space `k^m`. -/
39 def RowsSpan
40     (v : Fin r → Matrix (Fin d) (Fin m) k) : Prop :=
41   Submodule.span k
42       (Set.range (fun p : Fin r × Fin d ↦ v p.1 p.2)) = ⊤
43 
44 /--
45 Left module generation is exactly row spanning.  The assumption `0 < d` is
46 needed only in the forward direction, to read a row from a nonempty matrix.
47 -/
48 theorem leftGenerates_iff_rowsSpan
49     (hd : 0 < d) (v : Fin r → Matrix (Fin d) (Fin m) k) :
50     LeftGenerates v ↔ RowsSpan v := by
51   classical
52   constructor
53   · intro hgen
54     rw [RowsSpan]
55     apply top_unique
56     intro y _hy
57     let a₀ : Fin d := ⟨0, hd⟩
58     let X : Matrix (Fin d) (Fin m) k := fun _ ↦ y
59     obtain ⟨A, hA⟩ := hgen X
60     have hy : y = ∑ i, ∑ b, A i a₀ b • v i b := by
61       funext j
62       have hentry := congrFun (congrFun hA a₀) j
63       simpa [X, Matrix.sum_apply, Matrix.mul_apply, smul_eq_mul] using hentry
64     rw [hy]
65     apply Submodule.sum_mem
66     intro i _hi
67     apply Submodule.sum_mem
68     intro b _hb
69     exact Submodule.smul_mem _ _
70       (Submodule.subset_span (Set.mem_range_self (i, b)))
71   · intro hrows X
72     have hsurj :
73         ∀ y : Fin m → k,
74           ∃ c : Fin r × Fin d → k,
75             ∑ p, c p • v p.1 p.2 = y := by
76       have htop :
77           ⊤ ≤ Submodule.span k
78             (Set.range (fun p : Fin r × Fin d ↦ v p.1 p.2)) := by
79         simpa [RowsSpan] using hrows.symm.le
80       exact
81         (Submodule.top_le_span_range_iff_forall_exists_fun
82           (R := k) (v := fun p : Fin r × Fin d ↦ v p.1 p.2)).mp htop
83     choose c hc using fun a : Fin d ↦ hsurj (X a)
84     let A : Fin r → Matrix (Fin d) (Fin d) k :=
85       fun i a b ↦ c a (i, b)
86     refine ⟨A, ?_⟩
87     ext a j
88     have hrow := congrFun (hc a) j
89     rw [Matrix.sum_apply]
90     simp_rw [Matrix.mul_apply]
91     change X a j = ∑ i, ∑ b, c a (i, b) * v i b j
92     calc
93       X a j = ∑ p : Fin r × Fin d, c a p * v p.1 p.2 j := by
94         simpa [Pi.smul_apply, smul_eq_mul] using hrow.symm
95       _ = ∑ i, ∑ b, c a (i, b) * v i b j :=
96         Fintype.sum_prod_type _
97 
98 /-- Any `r` left generators force the multiplicity bound `m ≤ r * d`. -/
99 theorem multiplicity_le_of_leftGenerates
100     (hd : 0 < d) {v : Fin r → Matrix (Fin d) (Fin m) k}
101     (hgen : LeftGenerates v) :
102     m ≤ r * d := by
103   have hrows := (leftGenerates_iff_rowsSpan hd v).mp hgen
104   have hdim := finrank_le_of_span_eq_top (R := k) hrows
105   simpa [Module.finrank_pi, Fintype.card_prod] using hdim
106 
107 /--
108 If `m ≤ r * d`, an explicit family of `r` generators exists.  Its rows are
109 standard basis vectors, placed using an embedding `Fin m ↪ Fin r × Fin d`;
110 unused rows are zero.
111 -/
112 theorem exists_leftGenerators_of_le
113     (hd : 0 < d) (h : m ≤ r * d) :
114     ∃ v : Fin r → Matrix (Fin d) (Fin m) k, LeftGenerates v := by
115   classical
116   have he_nonempty : Nonempty (Fin m ↪ Fin r × Fin d) :=
117     Function.Embedding.nonempty_of_card_le (by simpa using h)
118   let e : Fin m ↪ Fin r × Fin d := Classical.choice he_nonempty
119   let v : Fin r → Matrix (Fin d) (Fin m) k :=
120     fun i a j ↦ if e j = (i, a) then 1 else 0
121   have hv_basis (j : Fin m) :
122       v (e j).1 (e j).2 = Pi.basisFun k (Fin m) j := by
123     funext q
124     simp [v, Pi.basisFun_apply, Pi.single_apply, e.injective.eq_iff]
125   refine ⟨v, (leftGenerates_iff_rowsSpan hd v).mpr ?_⟩
126   rw [RowsSpan]
127   apply top_unique
128   rw [← (Pi.basisFun k (Fin m)).span_eq]
129   apply Submodule.span_mono
130   rintro _ ⟨j, rfl⟩
131   exact ⟨e j, hv_basis j⟩
132 
133 /--
134 There exist `r` generators for `(k^d)^m` under `M_d(k)` exactly when
135 `m ≤ r * d`.
136 -/
137 theorem exists_leftGenerators_iff (hd : 0 < d) :
138     (∃ v : Fin r → Matrix (Fin d) (Fin m) k, LeftGenerates v) ↔
139       m ≤ r * d := by
140   constructor
141   · rintro ⟨v, hv⟩
142     exact multiplicity_le_of_leftGenerates hd hv
143   · exact exists_leftGenerators_of_le hd
144 
145 /--
146 The ceiling quotient `m ⌈/⌉ d` is the least number of generators of the
147 one-simple-block module `(k^d)^m`.
148 -/
149 theorem ceilDiv_isLeast_generatorCount (hd : 0 < d) :
150     IsLeast
151       {r : ℕ |
152         ∃ v : Fin r → Matrix (Fin d) (Fin m) k, LeftGenerates v}
153       (m ⌈/⌉ d) := by
154   constructor
155   · apply (exists_leftGenerators_iff (k := k) (r := m ⌈/⌉ d) hd).mpr
156     have hm : m ≤ d * (m ⌈/⌉ d) :=
157       (ceilDiv_le_iff_le_mul hd).mp le_rfl
158     simpa [Nat.mul_comm] using hm
159   · intro r hr
160     apply (ceilDiv_le_iff_le_mul hd).mpr
161     have hm := (exists_leftGenerators_iff (k := k) (r := r) hd).mp hr
162     simpa [Nat.mul_comm] using hm
163 
164 end Komorebi.SemisimpleSeedRank
165 
166 #print axioms Komorebi.SemisimpleSeedRank.leftGenerates_iff_rowsSpan
167 #print axioms Komorebi.SemisimpleSeedRank.exists_leftGenerators_iff
168 #print axioms Komorebi.SemisimpleSeedRank.ceilDiv_isLeast_generatorCount

Back to source controls