MatrixSpanExamples.lean

1 import PaperX.MatrixSpanBound
2 import PaperX.CertificateExamples
3 import Mathlib.GroupTheory.FreeGroup.Basic
4 
5 /-! A full-span 3-adic template with a genuine nonunit comparison.
6 The uniform theorem applies to every integral representation in its rational
7 isomorphism class, rather than just the displayed pair. -/
8 set_option autoImplicit false
9 namespace PaperX.MatrixSpanExamples
10 open scoped Matrix
11 open PaperX.RepresentationLimits PaperX.RepresentationClasses
12 variable {R : Type*} [CommRing R]
13 
14 def upper (a : R) : Matrix (Fin 2) (Fin 2) R := !![1, a; 0, 1]
15 def lower (a : R) : Matrix (Fin 2) (Fin 2) R := !![1, 0; a, 1]
16 
17 def upperUnit (a : R) : (Matrix (Fin 2) (Fin 2) R)ˣ where
18   val := upper a
19   inv := upper (-a)
20   val_inv := by ext i j; fin_cases i <;> fin_cases j <;>
21     simp [upper, Matrix.mul_apply, Fin.sum_univ_two]
22   inv_val := by ext i j; fin_cases i <;> fin_cases j <;>
23     simp [upper, Matrix.mul_apply, Fin.sum_univ_two]
24 
25 def lowerUnit (a : R) : (Matrix (Fin 2) (Fin 2) R)ˣ where
26   val := lower a
27   inv := lower (-a)
28   val_inv := by ext i j; fin_cases i <;> fin_cases j <;>
29     simp [lower, Matrix.mul_apply, Fin.sum_univ_two]
30   inv_val := by ext i j; fin_cases i <;> fin_cases j <;>
31     simp [lower, Matrix.mul_apply, Fin.sum_univ_two]
32 
33 def pairRep (a b : R) : MatrixRep R (FreeGroup (Fin 2)) (Fin 2) :=
34   (Units.coeHom _).comp (FreeGroup.lift fun i : Fin 2 =>
35     if i = 0 then upperUnit a else lowerUnit b)
36 
37 @[simp] theorem pairRep_zero (a b : R) :
38     pairRep a b (FreeGroup.of 0) = upper a := by
39   simp [pairRep, upperUnit]
40 
41 @[simp] theorem pairRep_one (a b : R) :
42     pairRep a b (FreeGroup.of 1) = lower b := by
43   simp [pairRep, lowerUnit]
44 
45 /-- The integral action span contains a times every matrix, proved directly
46 from the two generators and their product. -/
47 theorem scalar_matrix_mem_span (a : R) (M : Matrix (Fin 2) (Fin 2) R) :
48     a • M ∈ Submodule.span R (Set.range (pairRep a 1)) := by
49   let S := Submodule.span R (Set.range (pairRep a 1))
50   have hU : upper a ∈ S := by
51     apply Submodule.subset_span
52     exact ⟨FreeGroup.of 0, pairRep_zero a 1⟩
53   have hL : lower (1 : R) ∈ S := by
54     apply Submodule.subset_span
55     exact ⟨FreeGroup.of 1, pairRep_one a 1⟩
56   have hI : (1 : Matrix (Fin 2) (Fin 2) R) ∈ S := by
57     apply Submodule.subset_span
58     exact ⟨1, map_one _⟩
59   have hUL : upper a * lower 1 ∈ S := by
60     apply Submodule.subset_span
61     exact ⟨FreeGroup.of 0 * FreeGroup.of 1, by simp⟩
62   have h00 := S.add_mem (S.sub_mem (S.sub_mem hUL hU) hL) hI
63   have h01 := S.sub_mem hU hI
64   have h10 := S.sub_mem hL hI
65   have h11 := S.sub_mem (S.smul_mem a hI) h00
66   have hm : a • M =
67       M 0 0 • (upper a * lower 1 - upper a - lower 1 + 1) +
68       M 0 1 • (upper a - 1) + (a * M 1 0) • (lower 1 - 1) +
69       M 1 1 • (a • (1 : Matrix (Fin 2) (Fin 2) R) -
70         (upper a * lower 1 - upper a - lower 1 + 1)) := by
71     ext i j
72     fin_cases i <;> fin_cases j <;>
73       simp [upper, lower] <;> ring
74   rw [hm]
75   exact S.add_mem (S.add_mem (S.add_mem (S.smul_mem _ h00) (S.smul_mem _ h01))
76     (S.smul_mem _ h10)) (S.smul_mem _ h11)
77 
78 @[simp] theorem changeCoefficients_pairRep {S : Type*} [CommRing S]
79     (f : R →+* S) (a b : R) :
80     changeCoefficients f (pairRep a b) = pairRep (f a) (f b) := by
81   apply FreeGroup.ext_hom
82   intro i
83   fin_cases i <;> ext j k <;> fin_cases j <;> fin_cases k <;>
84     simp [upper, lower]
85 
86 /-- Over a field, the same explicit matrices span the complete matrix algebra. -/
87 theorem field_span_eq_top {K : Type*} [Field K] (a : K) (ha : a ≠ 0) :
88     Submodule.span K (Set.range (pairRep a 1)) = ⊤ := by
89   apply top_unique
90   intro M _
91   have h := (Submodule.span K (Set.range (pairRep a 1))).smul_mem a⁻¹
92     (scalar_matrix_mem_span a M)
93   simpa [smul_smul, ha] using h
94 
95 def comparison (a : R) : Matrix (Fin 2) (Fin 2) R := !![1, 0; 0, a]
96 
97 @[simp] theorem comparison_det (a : R) : (comparison a).det = a := by
98   simp [comparison, Matrix.det_fin_two]
99 
100 /-- The two actual representations are intertwined for every free-group word. -/
101 theorem comparison_intertwines (a : R) (g : FreeGroup (Fin 2)) :
102     pairRep 1 a g * comparison a = comparison a * pairRep a 1 g := by
103   induction g using FreeGroup.induction_on with
104   | one => simp
105   | of i =>
106       fin_cases i <;> ext j k <;> fin_cases j <;> fin_cases k <;>
107         simp [upper, lower, comparison]
108   | inv_of i hi =>
109       let x := FreeGroup.of i
110       change pairRep 1 a x⁻¹ * comparison a = comparison a * pairRep a 1 x⁻¹
111       calc
112         pairRep 1 a x⁻¹ * comparison a =
113             pairRep 1 a x⁻¹ * comparison a * (pairRep a 1 x * pairRep a 1 x⁻¹) := by
114           rw [← map_mul, mul_inv_cancel, map_one, mul_one]
115         _ = pairRep 1 a x⁻¹ * (comparison a * pairRep a 1 x) * pairRep a 1 x⁻¹ := by
116           simp only [mul_assoc]
117         _ = pairRep 1 a x⁻¹ * (pairRep 1 a x * comparison a) * pairRep a 1 x⁻¹ := by
118           rw [← hi]
119         _ = comparison a * pairRep a 1 x⁻¹ := by
120           rw [← mul_assoc, ← map_mul, inv_mul_cancel, map_one, one_mul]
121   | mul x y hx hy =>
122       simp only [map_mul]
123       calc
124         pairRep 1 a x * pairRep 1 a y * comparison a =
125           pairRep 1 a x * (comparison a * pairRep a 1 y) := by rw [mul_assoc, hy]
126         _ = comparison a * (pairRep a 1 x * pairRep a 1 y) := by rw [← mul_assoc, hx, mul_assoc]
127 
128 noncomputable def tau : MatrixRep ℤ_[3] (FreeGroup (Fin 2)) (Fin 2) := pairRep 3 1
129 noncomputable def rho : MatrixRep ℤ_[3] (FreeGroup (Fin 2)) (Fin 2) := pairRep 1 3
130 
131 /-- The actual 3-adic template has integral matrix-span exponent one. -/
132 theorem three_adic_span (M : Matrix (Fin 2) (Fin 2) ℤ_[3]) :
133     (3 : ℤ_[3]) • M ∈ Submodule.span ℤ_[3] (Set.range tau) :=
134   scalar_matrix_mem_span 3 M
135 
136 /-- The field span is verified from the actual generator matrices. -/
137 theorem three_adic_full_field_span :
138     Submodule.span ℚ_[3]
139       (Set.range (fun g => (tau g).map (algebraMap ℤ_[3] ℚ_[3]))) = ⊤ := by
140   have he : (fun g => (tau g).map (algebraMap ℤ_[3] ℚ_[3])) =
141       (pairRep (3 : ℚ_[3]) 1 : FreeGroup (Fin 2) → Matrix (Fin 2) (Fin 2) ℚ_[3]) := by
142     funext g
143     change changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) (pairRep 3 1) g = _
144     rw [changeCoefficients_pairRep, map_ofNat, map_one]
145   rw [he]
146   exact field_span_eq_top 3 (by norm_num)
147 
148 /-- The displayed comparison is nonsingular over Q_3. -/
149 theorem three_adic_field_conjugate :
150     Conjugate (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) tau)
151       (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) rho) := by
152   obtain ⟨u, _, hu⟩ := PaperX.CertificateIsomorphisms.exists_conjugating_unit
153     (algebraMap ℤ_[3] ℚ_[3]) (IsFractionRing.injective ℤ_[3] ℚ_[3])
154     rho tau (comparison 3) (by rw [comparison_det]; norm_num)
155     (comparison_intertwines 3)
156   exact ⟨u, hu⟩
157 
158 /-- One explicit depth works for the entire rational isomorphism class. -/
159 theorem every_conjugate_has_depth_three (σ : MatrixRep ℤ_[3] (FreeGroup (Fin 2)) (Fin 2))
160     (hσ : Conjugate (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) tau)
161       (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) σ)) :
162     ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[3], (∀ g, σ g * P = P * tau g) ∧
163       (P.map (Ideal.Quotient.mk ((Ideal.span {(3 : ℤ_[3])}) ^ 3))).det ≠ 0 := by
164   obtain ⟨u, hu⟩ := hσ
165   have hi : ∀ g, (σ g).map (algebraMap ℤ_[3] ℚ_[3]) * (u : Matrix (Fin 2) (Fin 2) ℚ_[3]) =
166       (u : Matrix (Fin 2) (Fin 2) ℚ_[3]) * (tau g).map (algebraMap ℤ_[3] ℚ_[3]) := by
167     intro g
168     have he := congrArg (fun r : MatrixRep ℚ_[3] (FreeGroup (Fin 2)) (Fin 2) => r g) hu
169     change (u : Matrix (Fin 2) (Fin 2) ℚ_[3]) * (tau g).map (algebraMap ℤ_[3] ℚ_[3]) *
170       (↑(u⁻¹) : Matrix (Fin 2) (Fin 2) ℚ_[3]) = (σ g).map (algebraMap ℤ_[3] ℚ_[3]) at he
171     rw [← he, mul_assoc, mul_assoc]
172     simp
173   have hh := PaperX.MatrixSpanBound.exists_bounded_comparison σ tau 3
174     (PadicInt.irreducible_p (p := 3)) 1 (by simpa using three_adic_span)
175     (u : Matrix (Fin 2) (Fin 2) ℚ_[3]) u.ne_zero hi
176   exact hh
177 
178 /-- The exhibited comparison is an integral nonunit. -/
179 theorem displayed_comparison_not_unit : ¬ IsUnit (comparison (3 : ℤ_[3])) := by
180   intro h
181   have hd := (Matrix.isUnit_iff_isUnit_det _).mp h
182   rw [comparison_det] at hd
183   exact (PadicInt.irreducible_p (p := 3)).not_isUnit hd
184 
185 /-- No alternative integral change of basis exists: the first named generator
186 is trivial modulo three for tau and nontrivial modulo three for rho. -/
187 theorem not_integrally_conjugate : ¬ Conjugate tau rho := by
188   intro hc
189   obtain ⟨u, hu⟩ := changeCoefficients_conjugacy
190     (PadicInt.toZMod : ℤ_[3] →+* ZMod 3) hc
191   have hτ : changeCoefficients (PadicInt.toZMod : ℤ_[3] →+* ZMod 3)
192       tau (FreeGroup.of 0) = 1 := by
193     ext i j
194     fin_cases i <;> fin_cases j <;> simp [tau, upper]
195     rw [map_ofNat]
196     decide +kernel
197   have hρ : changeCoefficients (PadicInt.toZMod : ℤ_[3] →+* ZMod 3)
198       rho (FreeGroup.of 0) 0 1 = 1 := by simp [rho, upper]
199   have he := congrArg (fun σ : MatrixRep (ZMod 3) (FreeGroup (Fin 2)) (Fin 2) =>
200     σ (FreeGroup.of 0)) hu
201   rw [conjugate_apply, hτ, mul_one] at he
202   simp only [Units.mul_inv] at he
203   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 3) => M 0 1) he
204   rw [hρ] at h01
205   simp at h01
206 
207 /-- A direct invocation of the uniform theorem for the displayed nonintegrally
208 conjugate pair. -/
209 theorem actual_nonunit_class_has_certificate :
210     ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[3], (∀ g, rho g * P = P * tau g) ∧
211       (P.map (Ideal.Quotient.mk ((Ideal.span {(3 : ℤ_[3])}) ^ 3))).det ≠ 0 :=
212   every_conjugate_has_depth_three rho three_adic_field_conjugate
213 
214 end PaperX.MatrixSpanExamples

Back to source controls