S3Detection.lean

1 import PaperXII.S3Standard
2 import Mathlib.RepresentationTheory.Irreducible
3 import Mathlib.LinearAlgebra.Matrix.Trace
4 
5 /-!
6 # Canonical spectral projectors detect the standard representation
7 
8 The projectors are the two-root Lagrange spectral projectors, with their
9 actual eigenspace action proved below. Four such projectors separate every
10 endomorphism. This is stronger than detection on the irreducible adjoint
11 subrepresentations required by adequacy.
12 -/
13 
14 namespace PaperXII.S3Detection
15 
16 open PaperXII.S3Standard
17 open scoped Matrix
18 
19 abbrev Mat (k : Type*) := Matrix (Fin 2) (Fin 2) k
20 
21 /-- The canonical projector onto the `α` eigenspace for an operator with
22 annihilating polynomial `(X-α)(X-β)` and distinct roots. -/
23 def CanonicalProjector {k : Type*} [Field k] (A : Mat k) (α β : k) (P : Mat k) : Prop :=
24   α ≠ β ∧ (A - α • 1) * (A - β • 1) = 0 ∧ P = (α - β)⁻¹ • (A - β • 1)
25 
26 variable {k : Type*} [Field k]
27 
28 theorem projector_fixed_iff {A P : Mat k} {α β : k}
29     (h : CanonicalProjector A α β P) (v : Space k) :
30     P *ᵥ v = v ↔ A *ᵥ v = α • v := by
31   have hab : α - β ≠ 0 := sub_ne_zero.mpr h.1
32   rw [h.2.2, Matrix.smul_mulVec, Matrix.sub_mulVec, Matrix.smul_mulVec,
33     Matrix.one_mulVec]
34   constructor
35   · intro hv
36     have hh := congrArg (fun w : Space k => (α - β) • w) hv
37     simp only [smul_smul, mul_inv_cancel₀ hab, one_smul] at hh
38     rw [sub_smul] at hh
39     exact sub_left_inj.mp hh
40   · intro hv
41     rw [hv, ← sub_smul, smul_smul, inv_mul_cancel₀ hab, one_smul]
42 
43 theorem projector_kills_other {A P : Mat k} {α β : k}
44     (h : CanonicalProjector A α β P) {v : Space k}
45     (hv : A *ᵥ v = β • v) : P *ᵥ v = 0 := by
46   rw [h.2.2, Matrix.smul_mulVec, Matrix.sub_mulVec, Matrix.smul_mulVec,
47     Matrix.one_mulVec, hv, sub_self, smul_zero]
48 
49 theorem projector_image_eigen {A P : Mat k} {α β : k}
50     (h : CanonicalProjector A α β P) (v : Space k) :
51     A *ᵥ (P *ᵥ v) = α • (P *ᵥ v) := by
52   have hz : (A - α • 1) *ᵥ ((A - β • 1) *ᵥ v) = 0 := by
53     rw [Matrix.mulVec_mulVec, h.2.1, Matrix.zero_mulVec]
54   rw [Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec] at hz
55   have he := sub_eq_zero.mp hz
56   rw [h.2.2, Matrix.smul_mulVec, Matrix.mulVec_smul, he, smul_comm]
57 
58 theorem projector_idempotent {A P : Mat k} {α β : k}
59     (h : CanonicalProjector A α β P) : P * P = P := by
60   apply Matrix.mulVec_injective
61   funext v
62   rw [← Matrix.mulVec_mulVec]
63   exact (projector_fixed_iff h _).2 (projector_image_eigen h v)
64 
65 /-- The image is exactly the `α` eigenspace, rather than merely an invariant summand. -/
66 theorem projector_image_iff {A P : Mat k} {α β : k}
67     (h : CanonicalProjector A α β P) (v : Space k) :
68     (∃ w, P *ᵥ w = v) ↔ A *ᵥ v = α • v := by
69   constructor
70   · rintro ⟨w, rfl⟩
71     exact projector_image_eigen h w
72   · intro hv
73     exact ⟨v, (projector_fixed_iff h v).2 hv⟩
74 
75 /-- The complementary component is an actual `β` eigenvector. -/
76 theorem projector_complement_eigen {A P : Mat k} {α β : k}
77     (h : CanonicalProjector A α β P) (v : Space k) :
78     A *ᵥ (v - P *ᵥ v) = β • (v - P *ᵥ v) := by
79   have hab : α - β ≠ 0 := sub_ne_zero.mpr h.1
80   have hh : (α - β) • (P *ᵥ v) = A *ᵥ v - β • v := by
81     rw [h.2.2, Matrix.smul_mulVec, smul_smul, mul_inv_cancel₀ hab,
82       one_smul, Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec]
83   rw [sub_smul] at hh
84   rw [Matrix.mulVec_sub, projector_image_eigen h v, smul_sub]
85   linear_combination -hh
86 
87 theorem projector_eigen_decomposition {A P : Mat k} {α β : k}
88     (h : CanonicalProjector A α β P) (v : Space k) :
89     ∃ vα vβ : Space k, v = vα + vβ ∧
90       A *ᵥ vα = α • vα ∧ A *ᵥ vβ = β • vβ := by
91   exact ⟨P *ᵥ v, v - P *ᵥ v, by abel,
92     projector_image_eigen h v, projector_complement_eigen h v⟩
93 
94 theorem power_mulVec_of_eigen {A : Mat k} {α : k} {v : Space k}
95     (hv : A *ᵥ v = α • v) (n : ℕ) : A ^ n *ᵥ v = α ^ n • v := by
96   induction n with
97   | zero => simp
98   | succ n ih =>
99     rw [pow_succ, ← Matrix.mulVec_mulVec, hv, Matrix.mulVec_smul, ih,
100       smul_smul, pow_succ]
101     congr 1
102     exact mul_comm _ _
103 
104 theorem shifted_power_mulVec_of_eigen {A : Mat k} {α : k} {v : Space k}
105     (hv : A *ᵥ v = α • v) (β : k) (n : ℕ) :
106     (A - β • 1) ^ n *ᵥ v = (α - β) ^ n • v := by
107   apply power_mulVec_of_eigen
108   rw [Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec, hv, sub_smul]
109 
110 theorem generalized_eigen_iff_projector_fixed {A P : Mat k} {α β : k}
111     (h : CanonicalProjector A α β P) (v : Space k) {n : ℕ} (hn : 0 < n) :
112     (A - α • 1) ^ n *ᵥ v = 0 ↔ P *ᵥ v = v := by
113   have hp := shifted_power_mulVec_of_eigen (projector_image_eigen h v) α n
114   have hq := shifted_power_mulVec_of_eigen (projector_complement_eigen h v) α n
115   have hz : (A - α • 1) ^ n *ᵥ (P *ᵥ v) = 0 := by
116     simpa [zero_pow (Nat.ne_of_gt hn)] using hp
117   have he : (A - α • 1) ^ n *ᵥ v = (β - α) ^ n • (v - P *ᵥ v) := by
118     rw [Matrix.mulVec_sub, hz, sub_zero] at hq
119     exact hq
120   rw [he]
121   constructor
122   · intro hv
123     have ha : (β - α) ^ n ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr h.1.symm)
124     have hv' : v - P *ᵥ v = 0 := (smul_eq_zero.mp hv).resolve_left ha
125     exact (sub_eq_zero.mp hv').symm
126   · intro hv
127     rw [hv, sub_self, smul_zero]
128 
129 theorem projector_kills_generalized_other {A P : Mat k} {α β : k}
130     (h : CanonicalProjector A α β P) (v : Space k) {n : ℕ} (hn : 0 < n)
131     (hv : (A - β • 1) ^ n *ᵥ v = 0) : P *ᵥ v = 0 := by
132   have hp := shifted_power_mulVec_of_eigen (projector_image_eigen h v) β n
133   have hq := shifted_power_mulVec_of_eigen (projector_complement_eigen h v) β n
134   have hz : (A - β • 1) ^ n *ᵥ (v - P *ᵥ v) = 0 := by
135     simpa [zero_pow (Nat.ne_of_gt hn)] using hq
136   rw [Matrix.mulVec_sub, hv, zero_sub, neg_eq_zero] at hz
137   rw [hz] at hp
138   exact (smul_eq_zero.mp hp.symm).resolve_left (pow_ne_zero _ (sub_ne_zero.mpr h.1))
139 
140 /-- The complementary projection has exactly the other eigenspace as image. -/
141 theorem projector_complement_image_iff {A P : Mat k} {α β : k}
142     (h : CanonicalProjector A α β P) (v : Space k) :
143     (∃ w, (1 - P) *ᵥ w = v) ↔ A *ᵥ v = β • v := by
144   constructor
145   · rintro ⟨w, rfl⟩
146     simpa only [Matrix.sub_mulVec, Matrix.one_mulVec] using projector_complement_eigen h w
147   · intro hv
148     refine ⟨v, ?_⟩
149     rw [Matrix.sub_mulVec, Matrix.one_mulVec, projector_kills_other h hv, sub_zero]
150 
151 /-- For every positive exponent, the generalized eigenspace is the actual
152 ordinary eigenspace, because the two roots are distinct. -/
153 theorem generalized_eigen_iff_eigen {A P : Mat k} {α β : k}
154     (h : CanonicalProjector A α β P) (v : Space k) {n : ℕ} (hn : 0 < n) :
155     (A - α • 1) ^ n *ᵥ v = 0 ↔ A *ᵥ v = α • v :=
156   (generalized_eigen_iff_projector_fixed h v hn).trans (projector_fixed_iff h v)
157 
158 /-- The explicitly constructed matrix is the projection onto every positive
159 order generalized eigenspace, not only the ordinary eigenspace. -/
160 theorem projector_generalized_image_iff {A P : Mat k} {α β : k}
161     (h : CanonicalProjector A α β P) (v : Space k) {n : ℕ} (hn : 0 < n) :
162     (∃ w, P *ᵥ w = v) ↔ (A - α • 1) ^ n *ᵥ v = 0 :=
163   (projector_image_iff h v).trans (generalized_eigen_iff_eigen h v hn).symm
164 
165 
166 abbrev F := ZMod 7
167 
168 
169 def Ps1 : Mat F := !![0, 4; 0, 1]
170 def Psminus : Mat F := !![1, 3; 0, 0]
171 def Pt2 : Mat F := !![2, 4; 3, 6]
172 def Pconj : Mat F := !![1, 0; 4, 0]
173 
174 theorem ps1_canonical :
175     CanonicalProjector (matrixRep F transposition) 1 (-1) Ps1 := by
176   rw [matrixRep_transposition]
177   unfold CanonicalProjector
178   decide +kernel
179 
180 theorem psminus_canonical :
181     CanonicalProjector (matrixRep F transposition) (-1) 1 Psminus := by
182   rw [matrixRep_transposition]
183   unfold CanonicalProjector
184   decide +kernel
185 
186 theorem pt2_canonical :
187     CanonicalProjector (matrixRep F cycle) 2 4 Pt2 := by
188   rw [matrixRep_cycle]
189   unfold CanonicalProjector
190   decide +kernel
191 
192 theorem pconj_canonical :
193     CanonicalProjector (matrixRep F (cycle * transposition * cycle⁻¹)) 1 (-1) Pconj := by
194   have hi : cycle⁻¹ = cycle * cycle := by decide +kernel
195   rw [hi]
196   simp only [map_mul]
197   rw [matrixRep_cycle, matrixRep_transposition]
198   unfold CanonicalProjector
199   decide +kernel
200 
201 
202 
203 /-- These four genuine eigenprojectors have a nondegenerate trace pairing
204 with the entire endomorphism algebra. -/
205 theorem trace_pairings_separate (W : Mat F)
206     (h1 : Matrix.trace (Ps1 * W) = 0)
207     (h2 : Matrix.trace (Psminus * W) = 0)
208     (h3 : Matrix.trace (Pt2 * W) = 0)
209     (h4 : Matrix.trace (Pconj * W) = 0) : W = 0 := by
210   simp [Matrix.trace, Matrix.vecMul, dotProduct, Fin.sum_univ_succ,
211     Ps1, Psminus, Pt2, Pconj] at h1 h2 h3 h4
212   ext i j
213   fin_cases i <;> fin_cases j <;> change _ = (0 : F)
214   · linear_combination (norm := ring_nf) 3 * h1 + 6 * h2 + 3 * h3 + 3 * h4
215     simp only [show (42 : F) = 0 from rfl, show (21 : F) = 0 from rfl,
216       show (15 : F) = 1 from rfl, mul_zero, mul_one, sub_zero]
217     exact sub_self _
218   · linear_combination (norm := ring_nf) h1 + 2 * h2 + h3 + 3 * h4
219     simp only [show (14 : F) = 0 from rfl, show (7 : F) = 0 from rfl,
220       show (15 : F) = 1 from rfl, mul_zero, mul_one, sub_zero]
221     exact sub_self _
222   · linear_combination (norm := ring_nf) 6 * h1 + 3 * h2 + 6 * h3 + 6 * h4
223     simp only [show (57 : F) = 1 from rfl, show (42 : F) = 0 from rfl,
224       show (21 : F) = 0 from rfl, mul_zero, mul_one, sub_zero]
225     exact sub_self _
226   · linear_combination (norm := ring_nf) 5 * h1 + 2 * h2 + 4 * h3 + 4 * h4
227     simp only [show (42 : F) = 0 from rfl, show (29 : F) = 1 from rfl,
228       show (14 : F) = 0 from rfl, show (28 : F) = 0 from rfl,
229       mul_zero, mul_one, sub_zero]
230     exact sub_self _
231 
232 /-- Every nonzero endomorphism is detected by an actual canonical
233 projector for an element of the represented group. -/
234 theorem detects_every_nonzero (W : Mat F) (hW : W ≠ 0) :
235     ∃ (g : Group) (α β : F) (P : Mat F),
236       CanonicalProjector (matrixRep F g) α β P ∧ Matrix.trace (P * W) ≠ 0 := by
237   by_cases h1 : Matrix.trace (Ps1 * W) = 0
238   · by_cases h2 : Matrix.trace (Psminus * W) = 0
239     · by_cases h3 : Matrix.trace (Pt2 * W) = 0
240       · refine ⟨cycle * transposition * cycle⁻¹, 1, -1, Pconj, pconj_canonical, ?_⟩
241         intro h4
242         exact hW (trace_pairings_separate W h1 h2 h3 h4)
243       · exact ⟨cycle, 2, 4, Pt2, pt2_canonical, h3⟩
244     · exact ⟨transposition, -1, 1, Psminus, psminus_canonical, h2⟩
245   · exact ⟨transposition, 1, -1, Ps1, ps1_canonical, h1⟩
246 
247 /-- The two displayed witnesses from the manuscript have their claimed traces. -/
248 theorem trace_sign_witness : Matrix.trace (Pt2 * !![2, 3; 4, 5]) = (3 : F) := by
249   decide +kernel
250 
251 theorem trace_standard_witness : Matrix.trace (Ps1 * !![6, 4; 3, 1]) = (6 : F) := by
252   decide +kernel
253 
254 /-- The group matrices linearly span the complete endomorphism algebra.
255 The sole characteristic restriction for this identity is `3 ≠ 0`. -/
256 theorem matrix_expansion (h3 : (3 : k) ≠ 0) (W : Mat k) :
257     W = ((W 0 0 - W 0 1 + W 1 0 + 2 * W 1 1) / 3) • matrixRep k 1 +
258       ((-W 0 0 + W 0 1 + 2 * W 1 0 + W 1 1) / 3) • matrixRep k transposition +
259       ((-W 0 0 - 2 * W 0 1 + 2 * W 1 0 + W 1 1) / 3) • matrixRep k cycle +
260       ((W 0 0 + 2 * W 0 1 + W 1 0 - W 1 1) / 3) •
261         matrixRep k (transposition * cycle) := by
262   simp only [map_one, map_mul, matrixRep_transposition, matrixRep_cycle]
263   ext i j
264   fin_cases i <;> fin_cases j <;>
265     simp <;>
266     field_simp <;> ring
267 
268 theorem all_matrices_preserve (h3 : (3 : k) ≠ 0)
269     (N : Subrepresentation (rep k)) {v : Space k} (hv : v ∈ N) (W : Mat k) :
270     W *ᵥ v ∈ N := by
271   rw [matrix_expansion h3 W]
272   simp only [Matrix.add_mulVec, Matrix.smul_mulVec, matrixRep_mulVec]
273   exact N.toSubmodule.add_mem
274     (N.toSubmodule.add_mem
275       (N.toSubmodule.add_mem (N.toSubmodule.smul_mem _ (N.apply_mem_toSubmodule 1 hv))
276         (N.toSubmodule.smul_mem _ (N.apply_mem_toSubmodule transposition hv)))
277       (N.toSubmodule.smul_mem _ (N.apply_mem_toSubmodule cycle hv)))
278     (N.toSubmodule.smul_mem _ (N.apply_mem_toSubmodule (transposition * cycle) hv))
279 
280 /-- Irreducibility over every field whose characteristic is not three. -/
281 theorem irreducible_of_three_ne_zero (h3 : (3 : k) ≠ 0) :
282     Representation.IsIrreducible (rep k) := by
283   have : Nontrivial (Subrepresentation (rep k)) :=
284     ⟨⟨⊥, ⊤, fun h => by
285       have hh : (fun _ : Fin 2 => (1 : k)) ∈ (⊥ : Subrepresentation (rep k)) := by
286         rw [h]
287         trivial
288       have hz : (fun _ : Fin 2 => (1 : k)) = 0 := hh
289       have hh' := congrFun hz 0
290       exact one_ne_zero hh'⟩⟩
291   apply IsSimpleOrder.of_forall_eq_top
292   intro N hN
293   have hN' : N.toSubmodule ≠ ⊥ := fun h =>
294     hN (Subrepresentation.toSubmodule_injective h)
295   obtain ⟨v, hv, hv0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hN'
296   obtain ⟨j, hj⟩ : ∃ j, v j ≠ 0 := by
297     by_contra! hn
298     exact hv0 (funext hn)
299   apply Subrepresentation.toSubmodule_injective
300   apply top_unique
301   intro w _
302   let W : Mat k := fun i l => if l = j then w i / v j else 0
303   have heq : W *ᵥ v = w := by
304     ext i
305     simp [W, Matrix.mulVec, dotProduct, hj]
306   rw [← heq]
307   exact all_matrices_preserve h3 N hv W
308 
309 /-- In particular the same representation is irreducible over every
310 characteristic-seven extension field, including an algebraic closure. -/
311 theorem irreducible_char_seven [CharP k 7] :
312     Representation.IsIrreducible (rep k) := by
313   apply irreducible_of_three_ne_zero
314   exact fun h => (by decide : ¬7 ∣ 3) ((CharP.cast_eq_zero_iff k 7 3).mp h)
315 
316 end PaperXII.S3Detection

Back to source controls