ClassFramingBoundary.lean

1 import PaperX.ClassCompletionExamples
2 
3 /-! Compatible classes do not make arbitrarily chosen matrix frames compatible.
4 The obstruction here is deliberately removable by an actual basis change. -/
5 set_option autoImplicit false
6 namespace PaperX.ClassFramingBoundary
7 open PaperX.RepresentationLimits PaperX.RepresentationClasses
8 open PaperX.CompletionExamples
9 open scoped Matrix
10 
11 def swapMatrix (R : Type) [CommRing R] : Matrix (Fin 2) (Fin 2) R := !![0,1;1,0]
12 
13 theorem swap_square (R : Type) [CommRing R] : swapMatrix R * swapMatrix R = 1 := by
14   ext i j
15   fin_cases i <;> fin_cases j <;>
16     simp [swapMatrix, Matrix.mul_apply, Fin.sum_univ_succ]
17 
18 def swapUnit (R : Type) [CommRing R] : (Matrix (Fin 2) (Fin 2) R)ˣ where
19   val := swapMatrix R
20   inv := swapMatrix R
21   val_inv := swap_square R
22   inv_val := swap_square R
23 
24 def reduceNine : ZMod 9 →+* ZMod 3 := ZMod.castHom (by decide) (ZMod 3)
25 
26 def lowerFrame : MatrixRep (ZMod 3) C2 (Fin 2) :=
27   changeCoefficients (Int.castRingHom (ZMod 3)) signRep
28 
29 def ordinaryUpper : MatrixRep (ZMod 9) C2 (Fin 2) :=
30   changeCoefficients (Int.castRingHom (ZMod 9)) signRep
31 
32 def chosenUpper : MatrixRep (ZMod 9) C2 (Fin 2) :=
33   conjugate (swapUnit (ZMod 9)) ordinaryUpper
34 
35 theorem lower_generator : lowerFrame generator = !![1,0;0,-1] := by decide +kernel
36 
37 theorem upper_generator : chosenUpper generator = !![-1,0;0,1] := by decide +kernel
38 
39 theorem lower_polynomial : (lowerFrame generator).charpoly = Polynomial.X^2-1 := by
40   change ((signRep generator).map (Int.castRingHom (ZMod 3))).charpoly = _
41   rw [Matrix.charpoly_map, integer_charpoly]
42   simp
43 
44 theorem upper_polynomial : (chosenUpper generator).charpoly = Polynomial.X^2-1 := by
45   rw [chosenUpper, PaperX.ClassInvariants.charpoly_conjugate]
46   change ((signRep generator).map (Int.castRingHom (ZMod 9))).charpoly = _
47   rw [Matrix.charpoly_map, integer_charpoly]
48   simp
49 
50 theorem ordinary_reduces : changeCoefficients reduceNine ordinaryUpper = lowerFrame := by
51   apply MonoidHom.ext
52   intro g
53   ext i j
54   simp [ordinaryUpper, lowerFrame, changeCoefficients_apply]
55 
56 theorem classes_compatible :
57     changeClassCoefficients reduceNine (classOf chosenUpper) = classOf lowerFrame := by
58   change classOf (changeCoefficients reduceNine chosenUpper) = classOf lowerFrame
59   apply classOf_eq.mpr
60   have h : Conjugate ordinaryUpper chosenUpper := ⟨swapUnit (ZMod 9), rfl⟩
61   have hr := changeCoefficients_conjugacy reduceNine h
62   rw [ordinary_reduces] at hr
63   exact conjugate_symm hr
64 
65 /-- The selected representative upstairs has swapped eigenlines, so its raw
66 matrix reduction differs from the selected representative downstairs. -/
67 theorem chosen_frames_incompatible : changeCoefficients reduceNine chosenUpper ≠ lowerFrame := by
68   intro h
69   have hc := congrArg (fun ρ : MatrixRep (ZMod 3) C2 (Fin 2) => ρ generator 0 0) h
70   have hn : changeCoefficients reduceNine chosenUpper generator 0 0 ≠
71       lowerFrame generator 0 0 := by decide +kernel
72   exact hn hc
73 
74 /-- A genuine change of basis repairs this mismatch. No lifting of arbitrary
75 invertible matrices is assumed. -/
76 theorem reframing_repairs :
77     changeCoefficients reduceNine (conjugate ((swapUnit (ZMod 9))⁻¹) chosenUpper) =
78       lowerFrame := by
79   rw [chosenUpper, ← conjugate_mul]
80   simp only [inv_mul_cancel, conjugate_one]
81   exact ordinary_reduces
82 
83 end PaperX.ClassFramingBoundary

Back to source controls