S3Spectrum.lean

1 import PaperXII.S3Standard
2 import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
3 import Mathlib.Algebra.Polynomial.Splits
4 
5 /-! The coefficient field contains every eigenvalue of the actual standard S3
6 representation. The factorizations cover all six permutations. -/
7 set_option autoImplicit false
8 namespace PaperXII.S3Spectrum
9 
10 open Matrix Polynomial S3Standard
11 
12 abbrev K := ZMod 7
13 
14 /-- Expand the two spectral factors without moving field arithmetic into polynomials. -/
15 theorem spectral_factors (a b : K) :
16     (X - C a) * (X - C b) = X ^ 2 - C (a + b) * X + C (a * b) := by
17   simp only [map_add, map_mul]
18   ring
19 
20 /-- The identity has the two expected unit eigenvalues. -/
21 theorem identity_charpoly : (matrixRep K (1 : Group)).charpoly = (X - 1) ^ 2 := by
22   rw [map_one, Matrix.charpoly_one]
23   rfl
24 
25 /-- The displayed transposition has eigenvalues 1 and -1. -/
26 theorem transposition_charpoly :
27     (matrixRep K transposition).charpoly = (X - C 1) * (X - C 6) := by
28   rw [matrixRep_transposition, Matrix.charpoly_fin_two]
29   rw [spectral_factors]
30   rw [show (1 + 6 : K) = 0 by decide, show (1 * 6 : K) = -1 by decide]
31   norm_num [Matrix.trace, Matrix.diag, Matrix.det_fin_two,
32     Matrix.mul_apply, Fin.sum_univ_succ, pow_two]
33 
34 /-- The displayed three-cycle splits already over F7. -/
35 theorem cycle_charpoly :
36     (matrixRep K cycle).charpoly = (X - C 2) * (X - C 4) := by
37   rw [matrixRep_cycle, Matrix.charpoly_fin_two]
38   rw [spectral_factors]
39   rw [show (2 + 4 : K) = -1 by decide, show (2 * 4 : K) = 1 by decide]
40   norm_num [Matrix.trace, Matrix.diag, Matrix.det_fin_two,
41     Matrix.mul_apply, Fin.sum_univ_succ, pow_two]
42 
43 /-- The inverse three-cycle has the same two eigenvalues. -/
44 theorem cycle_square_charpoly :
45     (matrixRep K (cycle ^ 2)).charpoly = (X - C 2) * (X - C 4) := by
46   rw [map_pow, matrixRep_cycle, Matrix.charpoly_fin_two]
47   rw [spectral_factors]
48   rw [show (2 + 4 : K) = -1 by decide, show (2 * 4 : K) = 1 by decide]
49   norm_num [Matrix.trace, Matrix.diag, Matrix.det_fin_two,
50     Matrix.mul_apply, Fin.sum_univ_succ, pow_two]
51 
52 /-- The second transposition has eigenvalues 1 and -1. -/
53 theorem transposition_cycle_charpoly :
54     (matrixRep K (transposition * cycle)).charpoly = (X - C 1) * (X - C 6) := by
55   rw [map_mul, matrixRep_transposition, matrixRep_cycle, Matrix.charpoly_fin_two]
56   rw [spectral_factors]
57   rw [show (1 + 6 : K) = 0 by decide, show (1 * 6 : K) = -1 by decide]
58   norm_num [Matrix.trace, Matrix.diag, Matrix.det_fin_two,
59     Matrix.mul_apply, Fin.sum_univ_succ, pow_two]
60 
61 /-- The third transposition has eigenvalues 1 and -1. -/
62 theorem transposition_cycle_square_charpoly :
63     (matrixRep K (transposition * cycle ^ 2)).charpoly = (X - C 1) * (X - C 6) := by
64   rw [map_mul, map_pow, matrixRep_transposition, matrixRep_cycle, Matrix.charpoly_fin_two]
65   rw [spectral_factors]
66   rw [show (1 + 6 : K) = 0 by decide, show (1 * 6 : K) = -1 by decide]
67   norm_num [Matrix.trace, Matrix.diag, Matrix.det_fin_two,
68     Matrix.mul_apply, Fin.sum_univ_succ, pow_two]
69 
70 /-- Every group element's characteristic polynomial splits over the actual coefficient field. -/
71 theorem all_charpolys_split (g : Group) : (matrixRep K g).charpoly.Splits := by
72   rcases group_cases g with rfl | rfl | rfl | rfl | rfl | rfl
73   · rw [identity_charpoly]
74     exact (Polynomial.Splits.X_sub_C (1 : K)).pow 2
75   · rw [transposition_charpoly]
76     exact (Polynomial.Splits.X_sub_C 1).mul (Polynomial.Splits.X_sub_C 6)
77   · rw [cycle_charpoly]
78     exact (Polynomial.Splits.X_sub_C 2).mul (Polynomial.Splits.X_sub_C 4)
79   · rw [cycle_square_charpoly]
80     exact (Polynomial.Splits.X_sub_C 2).mul (Polynomial.Splits.X_sub_C 4)
81   · rw [transposition_cycle_charpoly]
82     exact (Polynomial.Splits.X_sub_C 1).mul (Polynomial.Splits.X_sub_C 6)
83   · rw [transposition_cycle_square_charpoly]
84     exact (Polynomial.Splits.X_sub_C 1).mul (Polynomial.Splits.X_sub_C 6)
85 
86 end PaperXII.S3Spectrum

Back to source controls