PrecisionExamples.lean

1 import PaperX.ArithmeticCertificateExample
2 import PaperX.AveragingBoundary
3 import PaperX.PrecisionCompletion
4 
5 /-! Sharp finite precision examples over the actual ring Z_2. -/
6 set_option autoImplicit false
7 namespace PaperX.PrecisionExamples
8 open scoped Matrix
9 open PaperX.CompletionExamples PaperX.RepresentationLimits
10 open PaperX.RepresentationTopology PaperX.RepresentationClasses
11 open PaperX.RepresentationForests
12 
13 instance twoPrime : Fact (Nat.Prime 2) := ⟨by norm_num⟩
14 
15 def integerRho : MatrixRep ℤ C2 (Fin 2) where
16   toFun g := if g.toAdd = 0 then 1 else !![1, 2; 0, -1]
17   map_one' := by decide +kernel
18   map_mul' := by decide +kernel
19 
20 def integerLift : Matrix (Fin 2) (Fin 2) ℤ := !![1, 1; 0, 1]
21 def integerComparison : Matrix (Fin 2) (Fin 2) ℤ := !![1, -1; 0, 1]
22 
23 noncomputable def rho : MatrixRep ℤ_[2] C2 (Fin 2) :=
24   changeCoefficients (Int.castRingHom ℤ_[2]) integerRho
25 noncomputable def tau : MatrixRep ℤ_[2] C2 (Fin 2) :=
26   changeCoefficients (Int.castRingHom ℤ_[2]) signRep
27 noncomputable def initialLift : Matrix (Fin 2) (Fin 2) ℤ_[2] :=
28   integerLift.map (Int.castRingHom ℤ_[2])
29 noncomputable def comparison : Matrix (Fin 2) (Fin 2) ℤ_[2] :=
30   integerComparison.map (Int.castRingHom ℤ_[2])
31 
32 noncomputable abbrev modTwo : ℤ_[2] →+* ZMod 2 := PadicInt.toZMod
33 noncomputable abbrev modFour : ℤ_[2] →+* ZMod 4 := PadicInt.toZModPow 2
34 noncomputable abbrev twoIdeal : Ideal ℤ_[2] := Ideal.span {(2 : ℤ_[2])}
35 
36 /-- The actual p-adic quotient comparison agrees with reduction to Z/2^n. -/
37 theorem quotient_eq_iff (n : ℕ) (x y : ℤ_[2]) :
38     Ideal.Quotient.mk (twoIdeal^n) x = Ideal.Quotient.mk (twoIdeal^n) y ↔
39       PadicInt.toZModPow n x = PadicInt.toZModPow n y := by
40   rw [Ideal.Quotient.mk_eq_mk_iff_sub_mem, ← sub_eq_zero, ← map_sub,
41     ← RingHom.mem_ker, PadicInt.ker_toZModPow]
42   norm_num [twoIdeal, Ideal.span_singleton_pow]
43 
44 theorem quotient_matrices_eq_iff (n : ℕ) (A B : Matrix (Fin 2) (Fin 2) ℤ_[2]) :
45     A.map (Ideal.Quotient.mk (twoIdeal^n)) = B.map (Ideal.Quotient.mk (twoIdeal^n)) ↔
46       A.map (PadicInt.toZModPow n) = B.map (PadicInt.toZModPow n) := by
47   constructor
48   · intro h
49     ext i j
50     exact (quotient_eq_iff n _ _).mp (congrArg (fun M => M i j) h)
51   · intro h
52     ext i j
53     exact (quotient_eq_iff n _ _).mpr (congrArg (fun M => M i j) h)
54 
55 theorem group_order_nonzero : (Fintype.card C2 : ℤ_[2]) ≠ 0 := by
56   norm_num [show Fintype.card C2 = 2 from rfl]
57 
58 theorem group_order_not_unit : ¬ IsUnit (Fintype.card C2 : ℤ_[2]) := by
59   change ¬ IsUnit (2 : ℤ_[2])
60   exact PadicInt.irreducible_p.not_isUnit
61 
62 theorem group_order_divides_two : (Fintype.card C2 : ℤ_[2]) ∣ (2 : ℤ_[2])^1 := by
63   norm_num [show Fintype.card C2 = 2 from rfl]
64 
65 /-- The chosen lift is an exact intertwiner modulo four. -/
66 theorem initial_lift_intertwines_mod_four (g : C2) :
67     (rho g).map modFour * initialLift.map modFour =
68       initialLift.map modFour * (tau g).map modFour := by
69   have hi : ∀ g : C2,
70       (integerRho g).map (Int.castRingHom (ZMod 4)) *
71         integerLift.map (Int.castRingHom (ZMod 4)) =
72       integerLift.map (Int.castRingHom (ZMod 4)) *
73         (signRep g).map (Int.castRingHom (ZMod 4)) := by decide +kernel
74   simpa [rho, tau, initialLift, changeCoefficients, Matrix.map_map,
75     Function.comp_def] using hi g
76 
77 theorem initial_lift_intertwines_quotient (g : C2) :
78     (rho g).map (Ideal.Quotient.mk (twoIdeal^2)) *
79         initialLift.map (Ideal.Quotient.mk (twoIdeal^2)) =
80       initialLift.map (Ideal.Quotient.mk (twoIdeal^2)) *
81         (tau g).map (Ideal.Quotient.mk (twoIdeal^2)) := by
82   rw [← Matrix.map_mul, ← Matrix.map_mul]
83   apply (quotient_matrices_eq_iff 2 _ _).mpr
84   simpa only [Matrix.map_mul] using initial_lift_intertwines_mod_four g
85 
86 theorem initial_lift_not_intertwiner :
87     rho generator * initialLift ≠ initialLift * tau generator := by
88   intro h
89   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 0 1) h
90   norm_num [rho, tau, initialLift, integerLift, integerRho, signRep, signValue,
91     generator, changeCoefficients, Matrix.mul_apply, Fin.sum_univ_succ] at h01
92 
93 /-- Clearing the averaging denominator gives twice the displayed comparison. -/
94 theorem integer_averaging_sum :
95     (∑ g : C2, integerRho g * integerLift * signRep g⁻¹) =
96       (2 : ℤ) • integerComparison := by decide +kernel
97 
98 /-- The field-valued average is computed explicitly and is integral. -/
99 theorem rational_average_formula :
100     (2 : ℚ_[2])⁻¹ • (∑ g : C2,
101       (integerRho g).map (Int.castRingHom ℚ_[2]) *
102         integerLift.map (Int.castRingHom ℚ_[2]) *
103         (signRep g⁻¹).map (Int.castRingHom ℚ_[2])) =
104       integerComparison.map (Int.castRingHom ℚ_[2]) := by
105   have hs : (∑ g : C2,
106       (integerRho g).map (Int.castRingHom ℚ_[2]) *
107         integerLift.map (Int.castRingHom ℚ_[2]) *
108         (signRep g⁻¹).map (Int.castRingHom ℚ_[2])) =
109       !![(2 : ℚ_[2]), -2; 0, 2] := by
110     have h := congrArg (fun M => (Int.castRingHom ℚ_[2]).mapMatrix M) integer_averaging_sum
111     rw [map_sum] at h
112     simp only [map_mul, RingHom.mapMatrix_apply] at h
113     convert h using 1
114     ext i j
115     fin_cases i <;> fin_cases j <;> norm_num [integerComparison]
116   rw [hs]
117   ext i j
118   fin_cases i <;> fin_cases j <;> norm_num [integerComparison]
119 
120 theorem comparison_intertwines (g : C2) :
121     rho g * comparison = comparison * tau g := by
122   have hi : ∀ g : C2, integerRho g * integerComparison =
123       integerComparison * signRep g := by decide +kernel
124   have h := congrArg (fun M => (Int.castRingHom ℤ_[2]).mapMatrix M) (hi g)
125   change (integerRho g).map (Int.castRingHom ℤ_[2]) *
126     integerComparison.map (Int.castRingHom ℤ_[2]) =
127     integerComparison.map (Int.castRingHom ℤ_[2]) *
128       (signRep g).map (Int.castRingHom ℤ_[2])
129   simpa only [map_mul, RingHom.mapMatrix_apply] using h
130 
131 theorem comparison_det : comparison.det = 1 := by
132   norm_num [comparison, integerComparison, Matrix.det_fin_two]
133 
134 theorem comparison_isUnit : IsUnit comparison := by
135   apply (Matrix.isUnit_iff_isUnit_det _).mpr
136   rw [comparison_det]
137   exact isUnit_one
138 
139 theorem initial_lift_isUnit : IsUnit initialLift := by
140   apply (Matrix.isUnit_iff_isUnit_det _).mpr
141   have hd : initialLift.det = 1 := by
142     norm_num [initialLift, integerLift, Matrix.det_fin_two]
143   rw [hd]
144   exact isUnit_one
145 
146 theorem comparison_preserves_mod_two : comparison.map modTwo = initialLift.map modTwo := by
147   ext i j
148   fin_cases i <;> fin_cases j <;>
149     norm_num [comparison, initialLift, integerComparison, integerLift, Matrix.map_map]
150 
151 theorem comparison_changes_mod_four : comparison.map modFour ≠ initialLift.map modFour := by
152   intro h
153   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 4) => M 0 1) h
154   norm_num [comparison, initialLift, integerComparison, integerLift, Matrix.map_map] at h01
155   exact (by decide : (-1 : ZMod 4) ≠ 1) h01
156 
157 /-- No exact intertwiner, even a singular one, preserves this full mod-four lift.
158 The loss of one digit is forced by the example. -/
159 theorem no_exact_intertwiner_preserves_mod_four :
160     ¬ ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[2],
161       P.map modFour = initialLift.map modFour ∧
162       ∀ g, rho g * P = P * tau g := by
163   rintro ⟨P, hred, hP⟩
164   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 0 1) (hP generator)
165   norm_num [rho, tau, integerRho, signRep, signValue, generator,
166     changeCoefficients, Matrix.mul_apply, Fin.sum_univ_succ] at h01
167   have heq : 2 * (P 0 1 + P 1 1) = 0 := by linear_combination h01
168   have hsum : P 0 1 + P 1 1 = 0 := (mul_eq_zero.mp heq).resolve_left (by norm_num)
169   have hmod := congrArg modFour hsum
170   have hb := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 4) => M 0 1) hred
171   have hd := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 4) => M 1 1) hred
172   norm_num [initialLift, integerLift, Matrix.map_map] at hb hd
173   rw [map_add, map_zero, hb, hd] at hmod
174   norm_num at hmod
175   exact (by decide : (2 : ZMod 4) ≠ 0) hmod
176 
177 /-- The new precision theorem is instantiated on the prescribed mod-four matrix.
178 It retains exactly the guaranteed mod-two reduction. -/
179 theorem actual_two_adic_precision_lift :
180     ∃ P : (Matrix (Fin 2) (Fin 2) ℤ_[2])ˣ,
181       (P : Matrix (Fin 2) (Fin 2) ℤ_[2]).map (Ideal.Quotient.mk (twoIdeal^1)) =
182         initialLift.map (Ideal.Quotient.mk (twoIdeal^1)) ∧
183       ∀ g, rho g * (P : Matrix (Fin 2) (Fin 2) ℤ_[2]) =
184         (P : Matrix (Fin 2) (Fin 2) ℤ_[2]) * tau g := by
185   let f := Ideal.Quotient.mk (twoIdeal^2)
186   let B := Units.map f.mapMatrix.toMonoidHom initial_lift_isUnit.unit
187   have hBu : (B : Matrix (Fin 2) (Fin 2) (ℤ_[2] ⧸ twoIdeal^2)) = initialLift.map f := by
188     change (initial_lift_isUnit.unit : Matrix (Fin 2) (Fin 2) ℤ_[2]).map f = _
189     rw [initial_lift_isUnit.unit_spec]
190   obtain ⟨P, hP, hi⟩ := PrecisionAveraging.exists_isomorphism_lift (2 : ℤ_[2]) 1 1
191     rho tau group_order_nonzero group_order_divides_two
192     (by exact group_order_not_unit) (by decide) B (by
193       intro g
194       rw [hBu]
195       exact initial_lift_intertwines_quotient g)
196   refine ⟨P, ?_, hi⟩
197   rw [hP]
198   ext i j
199   simp [B, f]
200 
201 /-- For every pair of these rank-two C2 representations, mod four detects
202 integral isomorphism. No completeness or finite search is used in this application. -/
203 theorem two_adic_isomorphism_detected_mod_four
204     (σ υ : MatrixRep ℤ_[2] C2 (Fin 2)) :
205     Conjugate (reduce twoIdeal υ 2) (reduce twoIdeal σ 2) ↔ Conjugate υ σ := by
206   exact PrecisionAveraging.conjugacy_iff_reduction (2 : ℤ_[2]) 1 1 σ υ
207     group_order_nonzero group_order_divides_two (by exact group_order_not_unit) (by decide)
208 
209 theorem twoIdeal_eq_maximal : twoIdeal = IsLocalRing.maximalIdeal ℤ_[2] := by
210   exact PadicInt.maximalIdeal_eq_span_p.symm
211 
212 instance twoAdicComplete : IsAdicComplete twoIdeal ℤ_[2] := by
213   rw [twoIdeal_eq_maximal]
214   infer_instance
215 
216 instance twoResidueFinite : Finite (ℤ_[2] ⧸ twoIdeal) := by
217   rw [twoIdeal_eq_maximal]
218   exact Finite.of_equiv (ZMod 2) (PadicInt.residueField (p := 2)).symm.toEquiv
219 
220 /-- Concrete framed conditions populated by the displayed integral rho. -/
221 noncomputable def fixedConditions : Conditions (G := C2) (ι := Fin 2) twoIdeal where
222   allowed k σ := σ = reduce twoIdeal rho k
223   downward := by
224     intro j k hjk σ hσ
225     rw [hσ]
226     exact transition_reduce twoIdeal rho hjk
227 
228 /-- The type hypothesis is certified by the approximate lift A modulo four,
229 without using an already constructed exact comparison. -/
230 theorem fixed_finite_type : PrecisionCompletion.FiniteType (2 : ℤ_[2])
231     fixedConditions 1 tau := by
232   intro σ hσ
233   change σ = reduce twoIdeal rho 2 at hσ
234   subst σ
235   let f := Ideal.Quotient.mk (twoIdeal^2)
236   let B := Units.map f.mapMatrix.toMonoidHom initial_lift_isUnit.unit
237   refine ⟨B, ?_⟩
238   intro g
239   change (rho g).map f * (initial_lift_isUnit.unit : Matrix (Fin 2) (Fin 2) ℤ_[2]).map f =
240     (initial_lift_isUnit.unit : Matrix (Fin 2) (Fin 2) ℤ_[2]).map f * (tau g).map f
241   rw [initial_lift_isUnit.unit_spec]
242   exact initial_lift_intertwines_quotient g
243 
244 /-- The new completion theorem constructs a continuous integral realization
245 with the required integral type. The explicit rho supplies every-level occupancy. -/
246 theorem actual_two_adic_precision_completion :
247     ∃ (σ : MatrixRep ℤ_[2] C2 (Fin 2)) (P : (Matrix (Fin 2) (Fin 2) ℤ_[2])ˣ),
248       Realizes twoIdeal fixedConditions σ ∧ AdicRepContinuous twoIdeal σ ∧
249       (∀ g, σ g * (P : Matrix (Fin 2) (Fin 2) ℤ_[2]) =
250         (P : Matrix (Fin 2) (Fin 2) ℤ_[2]) * tau g) ∧
251       Ideal.Quotient.mk (twoIdeal^1) (P : Matrix (Fin 2) (Fin 2) ℤ_[2]).det ≠ 0 := by
252   apply PrecisionCompletion.continuous_finite_group_completion (2 : ℤ_[2]) fixedConditions
253     1 tau group_order_nonzero group_order_divides_two
254     (by exact group_order_not_unit) fixed_finite_type
255   · intro k
256     exact Ideal.finite_quotient_pow (IsNoetherian.noetherian twoIdeal) k
257   · intro k
258     exact ⟨reduce twoIdeal rho k, rfl⟩
259 
260 end PaperX.PrecisionExamples

Back to source controls