AveragingBoundary.lean

1 import PaperX.CompletionExamples
2 import PaperX.RepresentationClasses
3 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 
5 /-! A common residual representation is insufficient when the group order is
6 not a unit in the coefficient ring. This uses actual representations of C2. -/
7 set_option autoImplicit false
8 namespace PaperX.AveragingBoundary
9 open PaperX.RepresentationLimits PaperX.RepresentationClasses
10 open PaperX.CompletionExamples
11 open scoped Matrix
12 
13 noncomputable def signFour : MatrixRep (ZMod 4) C2 (Fin 2) :=
14   changeCoefficients (Int.castRingHom (ZMod 4)) signRep
15 
16 def trivialFour : MatrixRep (ZMod 4) C2 (Fin 2) := 1
17 
18 noncomputable def toTwo : ZMod 4 →+* ZMod 2 := ZMod.castHom (by decide) (ZMod 2)
19 
20 theorem same_residual : changeCoefficients toTwo signFour =
21     changeCoefficients toTwo trivialFour := by
22   apply MonoidHom.ext
23   intro g
24   ext i j
25   fin_cases i <;> fin_cases j <;>
26     simp [changeCoefficients, signFour, trivialFour, signRep, signValue, toTwo]
27   all_goals split_ifs <;> decide +kernel
28 
29 theorem group_order_not_unit : ¬ IsUnit (Fintype.card C2 : ZMod 4) := by
30   decide +kernel
31 
32 theorem signFour_det : (signFour generator).det = -1 := by
33   norm_num [signFour, changeCoefficients, signRep, signValue, generator,
34     Matrix.det_fin_two]
35 
36 theorem not_integrally_conjugate : ¬ Conjugate trivialFour signFour := by
37   rintro ⟨u, hu⟩
38   have h := congrArg (fun ρ : MatrixRep (ZMod 4) C2 (Fin 2) => ρ generator) hu
39   have htriv : trivialFour generator = 1 := rfl
40   rw [conjugate_apply, htriv, mul_one, Units.mul_inv] at h
41   have hd := congrArg Matrix.det h
42   rw [Matrix.det_one, signFour_det] at hd
43   exact (by decide : (1 : ZMod 4) ≠ -1) hd
44 
45 end PaperX.AveragingBoundary

Back to source controls