S3Adjoint.lean

1 import PaperXII.S3Standard
2 import Mathlib.LinearAlgebra.Trace
3 import Mathlib.RepresentationTheory.Subrepresentation
4 import Mathlib.GroupTheory.Perm.Sign
5 
6 /-!
7 # Trace-zero adjoint of the standard representation of S₃ over F₇
8 
9 The adjoint space is the actual kernel of matrix trace. Its action is actual
10 conjugation by the standard matrices. The displayed equivalence intertwines
11 the sign representation plus the standard representation with this action.
12 -/
13 
14 namespace PaperXII.S3Adjoint
15 
16 open S3Standard
17 
18 abbrev K := ZMod 7
19 abbrev Mat := Matrix (Fin 2) (Fin 2) K
20 
21 def traceZero : Submodule K Mat := LinearMap.ker (Matrix.traceLinearMap (Fin 2) K K)
22 
23 abbrev Adj := traceZero
24 
25 /-- The full conjugation representation on two-by-two matrices. -/
26 def conjugation : Representation K Group Mat where
27   toFun g := LinearMap.mulLeftRight K (matrixRep K g, matrixRep K g⁻¹)
28   map_one' := by ext X i j; simp [LinearMap.mulLeftRight]
29   map_mul' g h := by
30     ext X i j
31     simp [LinearMap.mulLeftRight, mul_assoc]
32 
33 @[simp] theorem conjugation_apply (g : Group) (X : Mat) :
34     conjugation g X = matrixRep K g * X * matrixRep K g⁻¹ := rfl
35 
36 /-- Trace-zero matrices are preserved by conjugation. -/
37 def adjointSubrepresentation : Subrepresentation conjugation where
38   toSubmodule := traceZero
39   apply_mem_toSubmodule g X hX := by
40     change Matrix.trace (matrixRep K g * X * matrixRep K g⁻¹) = 0
41     rw [Matrix.trace_mul_cycle]
42     rw [← map_mul, inv_mul_cancel, map_one, one_mul]
43     exact hX
44 
45 /-- The actual trace-zero adjoint representation. -/
46 def adjoint : Representation K Group Adj := adjointSubrepresentation.toRepresentation
47 
48 @[simp] theorem adjoint_apply (g : Group) (X : Adj) :
49     (adjoint g X : Mat) = matrixRep K g * X.val * matrixRep K g⁻¹ := rfl
50 
51 /-- Trace-zero matrix coordinates. -/
52 def W (a b c : K) : Mat := !![a, b; c, -a]
53 
54 @[simp] theorem trace_W (a b c : K) : Matrix.trace (W a b c) = 0 := by
55   simp [W, Matrix.trace, Fin.sum_univ_succ]
56 
57 /-- The scalar character is the actual permutation sign, reduced modulo 7. -/
58 def signValue (g : Group) : K := (((Equiv.Perm.sign g : ℤˣ) : ℤ) : K)
59 
60 @[simp] theorem signValue_one : signValue 1 = 1 := by simp [signValue]
61 
62 @[simp] theorem signValue_mul (g h : Group) :
63     signValue (g * h) = signValue g * signValue h := by simp [signValue]
64 
65 def signRep : Representation K Group K where
66   toFun g := signValue g • LinearMap.id
67   map_one' := by ext; simp
68   map_mul' g h := by ext; simp [mul_comm]
69 
70 @[simp] theorem signRep_apply (g : Group) (x : K) : signRep g x = signValue g * x := rfl
71 
72 /-- Columns `W(2,3,4)`, `W(1,1,2)`, `W(1,5,6)`. -/
73 def decompositionMap : (K × Space K) →ₗ[K] Adj where
74   toFun z := ⟨W (2*z.1 + z.2 0 + z.2 1) (3*z.1 + z.2 0 + 5*z.2 1)
75     (4*z.1 + 2*z.2 0 + 6*z.2 1), trace_W _ _ _⟩
76   map_add' z w := by
77     apply Subtype.ext
78     ext i j
79     fin_cases i <;> fin_cases j <;> simp [W] <;> ring
80   map_smul' c z := by
81     apply Subtype.ext
82     ext i j
83     fin_cases i <;> fin_cases j <;> simp [W] <;> ring
84 
85 /-- The inverse coefficients of the three displayed columns. -/
86 def decompositionInverse : Adj →ₗ[K] (K × Space K) where
87   toFun X := (X.val 0 0 + X.val 0 1 + 6 * X.val 1 0,
88     ![3 * X.val 0 0 + 5 * X.val 0 1, 3 * X.val 0 0 + 2 * X.val 1 0])
89   map_add' X Y := by
90     apply Prod.ext
91     · simp; ring
92     · ext i; fin_cases i <;> simp <;> ring
93   map_smul' c X := by
94     apply Prod.ext
95     · simp; ring
96     · ext i; fin_cases i <;> simp <;> ring
97 
98 theorem decompositionInverse_map (z : K × Space K) :
99     decompositionInverse (decompositionMap z) = z := by
100   apply Prod.ext
101   · change (2*z.1 + z.2 0 + z.2 1) + (3*z.1 + z.2 0 + 5*z.2 1) +
102       6*(4*z.1 + 2*z.2 0 + 6*z.2 1) = z.1
103     ring_nf
104     simp only [show (29 : K) = 1 by decide, show (14 : K) = 0 by decide,
105       show (42 : K) = 0 by decide]
106     simp
107   · ext i
108     fin_cases i <;> simp [decompositionMap, decompositionInverse, W] <;> ring_nf <;> simp only [show (21 : K) = 0 by decide, show (8 : K) = 1 by decide,
109       show (28 : K) = 0 by decide, show (14 : K) = 0 by decide,
110       show (7 : K) = 0 by decide, show (15 : K) = 1 by decide] <;> simp
111 
112 theorem decompositionMap_inverse (X : Adj) :
113     decompositionMap (decompositionInverse X) = X := by
114   have ht : X.val 0 0 + X.val 1 1 = 0 := by
115     simpa [traceZero, LinearMap.mem_ker, Matrix.trace, Fin.sum_univ_succ] using X.property
116   apply Subtype.ext
117   ext i j
118   fin_cases i <;> fin_cases j <;>
119     simp [decompositionMap, decompositionInverse, W] <;> ring_nf <;> simp only [show (21 : K) = 0 by decide, show (8 : K) = 1 by decide,
120       show (28 : K) = 0 by decide, show (14 : K) = 0 by decide,
121       show (7 : K) = 0 by decide, show (36 : K) = 1 by decide] <;> simp
122   exact neg_eq_iff_add_eq_zero.mpr ht
123 
124 /-- The full linear equivalence, before recording equivariance. -/
125 def decompositionLinearEquiv : (K × Space K) ≃ₗ[K] Adj :=
126   { decompositionMap with
127     invFun := decompositionInverse
128     left_inv := decompositionInverse_map
129     right_inv := decompositionMap_inverse }
130 
131 @[simp] theorem signValue_transposition : signValue transposition = -1 := by decide
132 
133 @[simp] theorem signValue_cycle : signValue cycle = 1 := by decide
134 
135 theorem decomposition_transposition (z : K × Space K) :
136     decompositionMap ((signRep.prod (rep K)) transposition z) =
137       adjoint transposition (decompositionMap z) := by
138   apply Subtype.ext
139   ext i j
140   fin_cases i <;> fin_cases j <;>
141     simp [decompositionMap, W, Representation.prod, signRep_apply,
142       adjoint_apply, transposition_inv, matrixRep_transposition, rep_transposition,
143       Matrix.toLin'_apply, Matrix.mul_apply, dotProduct,
144       Fin.sum_univ_succ] <;> apply sub_eq_zero.mp <;> ring_nf <;>
145     simp only [show (7 : K) = 0 by decide, show (14 : K) = 0 by decide] <;> simp
146 
147 theorem decomposition_cycle (z : K × Space K) :
148     decompositionMap ((signRep.prod (rep K)) cycle z) =
149       adjoint cycle (decompositionMap z) := by
150   apply Subtype.ext
151   ext i j
152   fin_cases i <;> fin_cases j <;>
153     simp [decompositionMap, W, Representation.prod, signRep_apply,
154       adjoint_apply, cycle_inv, matrixRep_cycle, rep_cycle, pow_two,
155       Matrix.toLin'_apply, Matrix.mul_apply, dotProduct,
156       Fin.sum_univ_succ] <;> apply sub_eq_zero.mp <;> ring_nf <;>
157     simp only [show (7 : K) = 0 by decide] <;> simp
158 
159 /-- The coordinate map intertwines the actions for every element of S₃. -/
160 theorem decomposition_equivariant (g : Group) (z : K × Space K) :
161     decompositionMap ((signRep.prod (rep K)) g z) = adjoint g (decompositionMap z) := by
162   have hm (g h : Group)
163       (hg : ∀ z, decompositionMap ((signRep.prod (rep K)) g z) = adjoint g (decompositionMap z))
164       (hh : ∀ z, decompositionMap ((signRep.prod (rep K)) h z) = adjoint h (decompositionMap z)) :
165       ∀ z, decompositionMap ((signRep.prod (rep K)) (g*h) z) =
166         adjoint (g*h) (decompositionMap z) := by
167     intro z
168     simp only [map_mul, Module.End.mul_apply]
169     rw [hg, hh]
170   have ht2 := hm cycle cycle decomposition_cycle decomposition_cycle
171   rw [← pow_two] at ht2
172   rcases group_cases g with h | h | h | h | h | h
173   · subst g; simp
174   · subst g; exact decomposition_transposition z
175   · subst g; exact decomposition_cycle z
176   · subst g; exact ht2 z
177   · subst g; exact hm transposition cycle decomposition_transposition decomposition_cycle z
178   · subst g; exact hm transposition (cycle ^ 2) decomposition_transposition ht2 z
179 
180 /-- The trace-zero adjoint is equivariantly the sign representation plus the standard representation. -/
181 noncomputable def decompositionEquiv : (signRep.prod (rep K)).Equiv adjoint :=
182   Representation.Equiv.mk decompositionLinearEquiv (by
183     intro g
184     apply LinearMap.ext
185     intro z
186     exact decomposition_equivariant g z)
187 
188 /-- Every invariant trace-zero matrix vanishes. -/
189 theorem fixed_eq_zero (X : Adj) (h : ∀ g, adjoint g X = X) : X = 0 := by
190   have hs := congrArg (fun Y : Adj => Y.val 1 0) (h transposition)
191   have ht := congrArg (fun Y : Adj => Y.val 0 0) (h cycle)
192   have hb := congrArg (fun Y : Adj => Y.val 0 1) (h transposition)
193   have htr : X.val 0 0 + X.val 1 1 = 0 := by
194     simpa [traceZero, LinearMap.mem_ker, Matrix.trace, Fin.sum_univ_succ] using X.property
195   simp [adjoint_apply, transposition_inv, matrixRep_transposition,
196     Matrix.mul_apply, Matrix.vecMul, dotProduct, Fin.sum_univ_succ] at hs hb
197   simp [adjoint_apply, cycle_inv, matrixRep_cycle, pow_two,
198     Matrix.mul_apply, Matrix.vecMul, dotProduct, Fin.sum_univ_succ] at ht
199   have hz (a : K) (ha : 2*a = 0) : a = 0 :=
200     (mul_eq_zero.mp ha).resolve_left (by decide)
201   have hc : X.val 1 0 = 0 := hz _ (by linear_combination -hs)
202   have ha : X.val 0 0 = 0 := hz _ (by linear_combination -ht + htr + hc)
203   have hd : X.val 1 1 = 0 := by linear_combination htr - ha
204   have hbb : X.val 0 1 = 0 := hz _ (by linear_combination -hb + hc - ha + hd)
205   apply Subtype.ext
206   ext i j
207   fin_cases i <;> fin_cases j <;> simp [ha, hbb, hc, hd]
208 
209 /-- The inclusion of the sign coordinates in the adjoint space. -/
210 def signEmbedding : K →ₗ[K] Adj := decompositionMap.comp (LinearMap.inl K K (Space K))
211 
212 /-- The inclusion of the standard coordinates in the adjoint space. -/
213 def standardEmbedding : Space K →ₗ[K] Adj :=
214   decompositionMap.comp (LinearMap.inr K K (Space K))
215 
216 /-- The actual sign subrepresentation of the trace-zero adjoint. -/
217 def signSummand : Subrepresentation adjoint where
218   toSubmodule := LinearMap.range signEmbedding
219   apply_mem_toSubmodule g X hX := by
220     obtain ⟨a, rfl⟩ := hX
221     refine ⟨signRep g a, ?_⟩
222     simpa [signEmbedding, Representation.prod] using decomposition_equivariant g (a, 0)
223 
224 /-- The actual standard subrepresentation of the trace-zero adjoint. -/
225 def standardSummand : Subrepresentation adjoint where
226   toSubmodule := LinearMap.range standardEmbedding
227   apply_mem_toSubmodule g X hX := by
228     obtain ⟨v, rfl⟩ := hX
229     refine ⟨rep K g v, ?_⟩
230     simpa [standardEmbedding, Representation.prod] using decomposition_equivariant g (0, v)
231 
232 /-- The paper's literal sign witness belongs to the sign subrepresentation. -/
233 theorem W_sign_mem : (⟨W 2 3 4, trace_W 2 3 4⟩ : Adj) ∈ signSummand := by
234   exact ⟨1, by decide⟩
235 
236 /-- The paper's literal standard witness belongs to the standard subrepresentation. -/
237 theorem W_standard_mem : (⟨W 6 4 3, trace_W 6 4 3⟩ : Adj) ∈ standardSummand := by
238   exact ⟨![3, 3], by decide⟩
239 
240 end PaperXII.S3Adjoint

Back to source controls