S3Standard.lean

1 import Mathlib.RepresentationTheory.Intertwining
2 import Mathlib.LinearAlgebra.Matrix.ToLin
3 import Mathlib.Algebra.Field.ZMod
4 import Mathlib.Tactic
5 
6 /-!
7 # The actual standard representation of `S₃`
8 
9 The coordinates used here are the basis `(1,-1,0), (0,1,-1)` of the
10 sum-zero submodule of the three-letter permutation representation.
11 All constructions work over an arbitrary commutative coefficient ring.
12 -/
13 
14 namespace PaperXII.S3Standard
15 
16 open Matrix
17 
18 instance primeSeven : Fact (Nat.Prime 7) := ⟨by decide⟩
19 
20 abbrev Group := Equiv.Perm (Fin 3)
21 abbrev Space (k : Type*) := Fin 2 → k
22 
23 variable (k : Type*) [CommRing k]
24 
25 /-- Coordinate inclusion into the three-letter permutation module. -/
26 def embed : Space k →ₗ[k] (Fin 3 → k) where
27   toFun v := ![v 0, -v 0 + v 1, -v 1]
28   map_add' v w := by ext i; fin_cases i <;> simp <;> ring
29   map_smul' c v := by ext i; fin_cases i <;> simp [mul_add]
30 
31 /-- The inverse coordinates on sum-zero vectors. -/
32 def project : (Fin 3 → k) →ₗ[k] Space k where
33   toFun w := ![w 0, -w 2]
34   map_add' v w := by ext i; fin_cases i <;> simp [add_comm]
35   map_smul' c v := by ext i; fin_cases i <;> simp
36 
37 @[simp] theorem project_embed (v : Space k) : project k (embed k v) = v := by
38   ext i
39   fin_cases i <;> simp [project, embed]
40 
41 theorem embed_sum_zero (v : Space k) : ∑ i, embed k v i = 0 := by
42   simp [embed, Fin.sum_univ_succ]
43 
44 theorem embed_project {w : Fin 3 → k} (hw : ∑ i, w i = 0) :
45     embed k (project k w) = w := by
46   have h : w 0 + w 1 + w 2 = 0 := by simpa [Fin.sum_univ_succ, add_assoc] using hw
47   ext i
48   fin_cases i <;> simp [embed, project]
49   linear_combination -h
50 
51 /-- The three-letter permutation representation. -/
52 def permutationRep : Representation k Group (Fin 3 → k) where
53   toFun g :=
54     { toFun := fun w i => w (g⁻¹ i)
55       map_add' := fun _ _ => rfl
56       map_smul' := fun _ _ => rfl }
57   map_one' := by ext w i; rfl
58   map_mul' g h := by ext w i; rfl
59 
60 theorem permutation_sum (g : Group) (w : Fin 3 → k) :
61     ∑ i, permutationRep k g w i = ∑ i, w i := by
62   exact Equiv.sum_comp g.symm w
63 
64 /-- The standard representation in the displayed two-dimensional coordinates. -/
65 def rep : Representation k Group (Space k) where
66   toFun g := (project k).comp ((permutationRep k g).comp (embed k))
67   map_one' := by
68     apply LinearMap.ext
69     intro v
70     exact project_embed k v
71   map_mul' g h := by
72     apply LinearMap.ext
73     intro v
74     funext i
75     change project k (permutationRep k (g * h) (embed k v)) i =
76       project k (permutationRep k g (embed k (project k (permutationRep k h (embed k v))))) i
77     rw [embed_project k (by rw [permutation_sum, embed_sum_zero])]
78     rfl
79 
80 theorem rep_apply (g : Group) (v : Space k) :
81     rep k g v = project k (permutationRep k g (embed k v)) := rfl
82 
83 theorem embed_rep (g : Group) (v : Space k) :
84     embed k (rep k g v) = permutationRep k g (embed k v) := by
85   change embed k (project k (permutationRep k g (embed k v))) = _
86   exact embed_project k (by rw [permutation_sum, embed_sum_zero])
87 
88 /-- The corresponding actual matrix representation. -/
89 def matrixRep : Group →* Matrix (Fin 2) (Fin 2) k :=
90   LinearMap.toMatrixAlgEquiv'.toMonoidHom.comp (rep k)
91 
92 theorem matrixRep_mulVec (g : Group) (v : Space k) :
93     matrixRep k g *ᵥ v = rep k g v := by
94   exact LinearMap.toMatrix'_mulVec (rep k g) v
95 
96 def transposition : Group := Equiv.swap 0 1
97 def cycle : Group := Equiv.swap 0 1 * Equiv.swap 1 2
98 
99 @[simp] theorem transposition_inv_zero : transposition⁻¹ (0 : Fin 3) = 1 := by decide
100 @[simp] theorem transposition_inv_two : transposition⁻¹ (2 : Fin 3) = 2 := by decide
101 @[simp] theorem cycle_inv_zero : cycle⁻¹ (0 : Fin 3) = 2 := by decide
102 @[simp] theorem cycle_inv_two : cycle⁻¹ (2 : Fin 3) = 1 := by decide
103 
104 theorem group_cases (g : Group) :
105     g = 1 ∨ g = transposition ∨ g = cycle ∨ g = cycle ^ 2 ∨
106       g = transposition * cycle ∨ g = transposition * cycle ^ 2 := by
107   revert g
108   decide
109 
110 theorem transposition_inv : transposition⁻¹ = transposition := by decide
111 theorem cycle_inv : cycle⁻¹ = cycle ^ 2 := by decide
112 
113 theorem rep_transposition :
114     rep k transposition = Matrix.toLin' !![-1, 1; 0, 1] := by
115   apply LinearMap.ext
116   intro v
117   change ![embed k v (transposition⁻¹ (0 : Fin 3)),
118     -(embed k v (transposition⁻¹ (2 : Fin 3)))] = _
119   rw [transposition_inv_zero, transposition_inv_two]
120   ext i
121   fin_cases i <;> simp [embed, Matrix.toLin'_apply, Matrix.mulVec, dotProduct,
122     Fin.sum_univ_succ, Matrix.cons_val]
123 
124 theorem rep_cycle : rep k cycle = Matrix.toLin' !![0, -1; 1, -1] := by
125   apply LinearMap.ext
126   intro v
127   change ![embed k v (cycle⁻¹ (0 : Fin 3)), -(embed k v (cycle⁻¹ (2 : Fin 3)))] = _
128   rw [cycle_inv_zero, cycle_inv_two]
129   ext i
130   fin_cases i <;> simp [embed, Matrix.toLin'_apply, Matrix.mulVec, dotProduct,
131     Fin.sum_univ_succ, Matrix.cons_val, add_comm]
132 
133 theorem matrixRep_transposition : matrixRep k transposition = !![-1, 1; 0, 1] := by
134   change LinearMap.toMatrix' (rep k transposition) = _
135   rw [rep_transposition, LinearMap.toMatrix'_toLin']
136 
137 theorem matrixRep_cycle : matrixRep k cycle = !![0, -1; 1, -1] := by
138   change LinearMap.toMatrix' (rep k cycle) = _
139   rw [rep_cycle, LinearMap.toMatrix'_toLin']
140 
141 /-- The actual sum-zero submodule in the permutation module. -/
142 def sumZero : Submodule k (Fin 3 → k) where
143   carrier := {w | ∑ i, w i = 0}
144   zero_mem' := by simp
145   add_mem' hx hy := by
146     change ∑ i, _ = 0 at hx hy ⊢
147     simp only [Pi.add_apply, Finset.sum_add_distrib, hx, hy, add_zero]
148   smul_mem' c w hw := by
149     change ∑ i, w i = 0 at hw
150     change ∑ i, c • w i = 0
151     rw [← Finset.smul_sum, hw, smul_zero]
152 
153 /-- The displayed coordinates give a linear equivalence onto all sum-zero vectors. -/
154 def sumZeroEquiv : Space k ≃ₗ[k] sumZero k where
155   toFun v := ⟨embed k v, embed_sum_zero k v⟩
156   invFun w := project k w
157   left_inv := project_embed k
158   right_inv w := by apply Subtype.ext; exact embed_project k w.property
159   map_add' v w := by apply Subtype.ext; exact (embed k).map_add v w
160   map_smul' c v := by apply Subtype.ext; exact (embed k).map_smul c v
161 
162 @[simp] theorem sumZeroEquiv_coe (v : Space k) :
163     (sumZeroEquiv k v : Fin 3 → k) = embed k v := rfl
164 
165 /-- Restriction of the permutation action to its actual sum-zero submodule. -/
166 def standardRep : Representation k Group (sumZero k) where
167   toFun g :=
168     { toFun := fun w => ⟨permutationRep k g w, by
169         change ∑ i, permutationRep k g w i = 0
170         rw [permutation_sum]
171         exact w.property⟩
172       map_add' := fun _ _ => rfl
173       map_smul' := fun _ _ => rfl }
174   map_one' := by apply LinearMap.ext; intro w; apply Subtype.ext; rfl
175   map_mul' g h := by apply LinearMap.ext; intro w; apply Subtype.ext; rfl
176 
177 /-- Equivalence with the actual standard representation, including equivariance. -/
178 def standardEquiv : (rep k).Equiv (standardRep k) :=
179   Representation.Equiv.mk (sumZeroEquiv k) (by
180     intro g
181     apply LinearMap.ext
182     intro v
183     apply Subtype.ext
184     exact embed_rep k g v)
185 
186 /-- The matrix representation is faithful over every nontrivial coefficient ring. -/
187 theorem matrixRep_faithful [Nontrivial k] : Function.Injective (matrixRep k) := by
188   apply (injective_iff_map_eq_one (matrixRep k)).2
189   intro g hg
190   have h01 := congrArg (fun A : Matrix (Fin 2) (Fin 2) k => A 0 1) hg
191   have h10 := congrArg (fun A : Matrix (Fin 2) (Fin 2) k => A 1 0) hg
192   rcases group_cases g with h | h | h | h | h | h
193   · exact h
194   all_goals subst g
195   all_goals norm_num [map_mul, map_pow, matrixRep_transposition, matrixRep_cycle,
196     Matrix.mul_apply, Fin.sum_univ_succ, pow_two] at h01
197   all_goals norm_num [map_mul, map_pow, matrixRep_transposition, matrixRep_cycle,
198     Matrix.mul_apply, Fin.sum_univ_succ, pow_two] at h10
199 
200 theorem rep_faithful [Nontrivial k] : Function.Injective (rep k) := by
201   intro g h hgh
202   apply matrixRep_faithful k
203   exact congrArg LinearMap.toMatrix' hgh
204 
205 /-- Coefficient extension agrees with the same standard matrices over the new ring. -/
206 theorem matrixRep_map {l : Type*} [CommRing l] (f : k →+* l) (g : Group) :
207     (matrixRep k g).map f = matrixRep l g := by
208   have hs : (!![-1, 1; 0, 1] : Matrix (Fin 2) (Fin 2) k).map f =
209       (!![-1, 1; 0, 1] : Matrix (Fin 2) (Fin 2) l) := by
210     ext i j
211     fin_cases i <;> fin_cases j <;> simp
212   have ht : (!![0, -1; 1, -1] : Matrix (Fin 2) (Fin 2) k).map f =
213       (!![0, -1; 1, -1] : Matrix (Fin 2) (Fin 2) l) := by
214     ext i j
215     fin_cases i <;> fin_cases j <;> simp
216   rcases group_cases g with h | h | h | h | h | h
217   all_goals subst g
218   all_goals simp only [map_one, map_mul, map_pow, matrixRep_transposition, matrixRep_cycle,
219     Matrix.map_mul, Matrix.map_pow, Matrix.map_one _ f.map_zero f.map_one, hs, ht]
220 
221 end PaperXII.S3Standard

Back to source controls