PrecisionBoundary.lean

1 import PaperX.PrecisionExamples
2 
3 /-! Residual equality modulo two does not determine an integral C2 representation,
4 even for actual continuous representations on finite free Z_2 modules. -/
5 set_option autoImplicit false
6 namespace PaperX.PrecisionBoundary
7 open scoped Matrix
8 open PaperX.CompletionExamples PaperX.RepresentationLimits
9 open PaperX.RepresentationTopology PaperX.RepresentationClasses
10 open PaperX.PrecisionExamples
11 
12 noncomputable def trivial : MatrixRep ℤ_[2] C2 (Fin 2) := 1
13 
14 theorem sign_and_trivial_same_mod_two : changeCoefficients modTwo tau =
15     changeCoefficients modTwo trivial := by
16   apply MonoidHom.ext
17   intro g
18   ext i j
19   fin_cases i <;> fin_cases j <;>
20     simp [changeCoefficients, tau, trivial, signRep, signValue]
21   all_goals split_ifs <;> simp
22 
23 theorem sign_generator_det : (tau generator).det = -1 := by
24   norm_num [tau, changeCoefficients, signRep, signValue, generator,
25     Matrix.det_fin_two]
26 
27 theorem sign_not_integrally_conjugate_trivial : ¬ Conjugate trivial tau := by
28   rintro ⟨u, hu⟩
29   have h := congrArg (fun ρ : MatrixRep ℤ_[2] C2 (Fin 2) => ρ generator) hu
30   have htriv : trivial generator = 1 := rfl
31   rw [conjugate_apply, htriv, mul_one, Units.mul_inv] at h
32   have hd := congrArg Matrix.det h
33   rw [Matrix.det_one, sign_generator_det] at hd
34   norm_num at hd
35 
36 theorem sign_continuous : AdicRepContinuous twoIdeal tau := by
37   let : TopologicalSpace ℤ_[2] := twoIdeal.adicTopology
38   exact continuous_of_discreteTopology
39 
40 theorem trivial_continuous : AdicRepContinuous twoIdeal trivial := by
41   let : TopologicalSpace ℤ_[2] := twoIdeal.adicTopology
42   exact continuous_of_discreteTopology
43 
44 /-- Modulo four already separates these two actual integral representations. -/
45 theorem sign_and_trivial_not_conjugate_mod_four :
46     ¬ Conjugate (changeCoefficients modFour trivial) (changeCoefficients modFour tau) := by
47   rintro ⟨u, hu⟩
48   have h := congrArg (fun ρ : MatrixRep (ZMod 4) C2 (Fin 2) => ρ generator) hu
49   rw [conjugate_apply] at h
50   have htriv : (changeCoefficients modFour trivial) generator = 1 := by
51     simp [changeCoefficients, trivial]
52   rw [htriv, mul_one, Units.mul_inv] at h
53   have hd := congrArg Matrix.det h
54   rw [Matrix.det_one] at hd
55   have hs : ((changeCoefficients modFour tau) generator).det = -1 := by
56     change (modFour.mapMatrix (tau generator)).det = _
57     rw [← RingHom.map_det, sign_generator_det]
58     simp
59   rw [hs] at hd
60   exact (by decide : (1 : ZMod 4) ≠ -1) hd
61 
62 end PaperX.PrecisionBoundary

Back to source controls