AveragingExamples.lean

1 import PaperX.AveragingCompletion
2 import PaperX.ArithmeticCertificateExample
3 
4 /-! A nontrivial integral comparison obtained by averaging for C2 over Z_3,
5 and its pullback to the actual absolute Galois group of Q. -/
6 set_option autoImplicit false
7 namespace PaperX.AveragingExamples
8 open scoped Matrix
9 open PaperX.CompletionExamples PaperX.RepresentationLimits
10 open PaperX.RepresentationTopology PaperX.RepresentationClasses
11 open PaperX.FiniteGroupAveraging PaperX.RepresentationForests
12 
13 def integerRho : MatrixRep ℤ C2 (Fin 2) where
14   toFun g := if g.toAdd = 0 then 1 else !![1, 1; 0, -1]
15   map_one' := by decide +kernel
16   map_mul' := by decide +kernel
17 
18 def integerLift : Matrix (Fin 2) (Fin 2) ℤ := !![1, 1; 0, 1]
19 
20 noncomputable def rho : MatrixRep ℤ_[3] C2 (Fin 2) :=
21   changeCoefficients (Int.castRingHom ℤ_[3]) integerRho
22 
23 noncomputable def tau : MatrixRep ℤ_[3] C2 (Fin 2) :=
24   changeCoefficients (Int.castRingHom ℤ_[3]) signRep
25 
26 noncomputable def initialLift : Matrix (Fin 2) (Fin 2) ℤ_[3] :=
27   integerLift.map (Int.castRingHom ℤ_[3])
28 
29 noncomputable abbrev residueMap : ℤ_[3] →+* ZMod 3 := PadicInt.toZMod
30 
31 theorem residue_surjective : Function.Surjective residueMap :=
32   ZMod.ringHom_surjective residueMap
33 
34 instance residueLocal : IsLocalHom residueMap :=
35   IsLocalHom.of_surjective residueMap residue_surjective
36 
37 theorem group_order_unit : IsUnit (Fintype.card C2 : ℤ_[3]) := by
38   apply isUnit_of_map_unit residueMap
39   rw [map_natCast, show Fintype.card C2 = 2 from rfl]
40   exact isUnit_iff_ne_zero.mpr (by decide +kernel)
41 
42 /-- The original lift is not an integral intertwiner. -/
43 theorem initial_lift_not_intertwiner :
44     rho generator * initialLift ≠ initialLift * tau generator := by
45   intro h
46   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[3] => M 0 1) h
47   norm_num [rho, tau, initialLift, integerLift, integerRho, signRep, signValue,
48     generator, changeCoefficients, Matrix.mul_apply, Fin.sum_univ_succ] at h01
49 
50 /-- Nevertheless its reduction is an exact residual intertwiner. -/
51 theorem residual_intertwining (g : C2) :
52     (rho g).map residueMap * initialLift.map residueMap =
53       initialLift.map residueMap * (tau g).map residueMap := by
54   have hi : ∀ g : C2,
55       (integerRho g).map (Int.castRingHom (ZMod 3)) *
56         integerLift.map (Int.castRingHom (ZMod 3)) =
57       integerLift.map (Int.castRingHom (ZMod 3)) *
58         (signRep g).map (Int.castRingHom (ZMod 3)) := by decide +kernel
59   simpa [rho, tau, initialLift, changeCoefficients, Matrix.map_map,
60     Function.comp_def] using hi g
61 
62 theorem initial_lift_unit : IsUnit initialLift := by
63   apply (Matrix.isUnit_iff_isUnit_det _).mpr
64   have hd : initialLift.det = 1 := by
65     norm_num [initialLift, integerLift, Matrix.det_fin_two]
66   rw [hd]
67   exact isUnit_one
68 
69 /-- The displayed average is an actual integral operator. -/
70 noncomputable def averagedComparison : Matrix (Fin 2) (Fin 2) ℤ_[3] :=
71   average rho tau group_order_unit initialLift
72 
73 theorem averaged_intertwining (g : C2) :
74     rho g * averagedComparison = averagedComparison * tau g :=
75   average_intertwines rho tau group_order_unit initialLift g
76 
77 theorem averaged_reduction : averagedComparison.map residueMap = initialLift.map residueMap :=
78   map_average_of_intertwines residueMap rho tau group_order_unit initialLift residual_intertwining
79 
80 theorem averaged_isUnit : IsUnit averagedComparison := by
81   apply matrix_isUnit_of_map residueMap
82   rw [averaged_reduction]
83   exact initial_lift_unit.map residueMap.mapMatrix
84 
85 theorem average_changes_the_lift : averagedComparison ≠ initialLift := by
86   intro h
87   exact initial_lift_not_intertwiner (h ▸ averaged_intertwining generator)
88 
89 /-- The explicit finite sum is evaluated over the integers first. -/
90 theorem integer_averaging_sum :
91     (∑ g : C2, integerRho g * integerLift * signRep g⁻¹) = !![2, -1; 0, 2] := by
92   decide +kernel
93 
94 /-- The constructed average is the integral matrix with upper-right entry
95 minus the inverse of two. This inverse exists inside Z_3. -/
96 theorem averaged_formula : averagedComparison =
97     !![1, -(↑(group_order_unit.unit⁻¹) : ℤ_[3]); 0, 1] := by
98   have hs : (∑ g : C2, rho g * initialLift * tau g⁻¹) =
99       !![(2 : ℤ_[3]), -1; 0, 2] := by
100     have hh := congrArg (fun M => (Int.castRingHom ℤ_[3]).mapMatrix M) integer_averaging_sum
101     rw [map_sum] at hh
102     simp only [map_mul, RingHom.mapMatrix_apply] at hh
103     convert hh using 1 <;> ext i j <;> fin_cases i <;> fin_cases j <;>
104       norm_num [rho, tau, initialLift, changeCoefficients]
105   have hi : (↑(group_order_unit.unit⁻¹) : ℤ_[3]) * 2 = 1 := by
106     calc
107       _ = (↑(group_order_unit.unit⁻¹) : ℤ_[3]) * (↑group_order_unit.unit : ℤ_[3]) :=
108         congrArg (fun x : ℤ_[3] => (↑(group_order_unit.unit⁻¹) : ℤ_[3]) * x)
109           group_order_unit.unit_spec.symm
110       _ = 1 := group_order_unit.unit.inv_mul
111   unfold averagedComparison average
112   rw [hs]
113   ext i j
114   fin_cases i <;> fin_cases j <;> simp_all
115 
116 theorem averaged_det_one : averagedComparison.det = 1 := by
117   rw [averaged_formula, Matrix.det_fin_two]
118   simp
119 
120 /-- This invokes the new existence theorem on the prescribed residual matrix.
121 It proves both integral invertibility and exact preservation of that matrix. -/
122 theorem actual_three_adic_isomorphism_lift :
123     ∃ P : (Matrix (Fin 2) (Fin 2) ℤ_[3])ˣ,
124       (P : Matrix (Fin 2) (Fin 2) ℤ_[3]).map residueMap = initialLift.map residueMap ∧
125       ∀ g, rho g * (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) =
126         (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) * tau g := by
127   let B := (initial_lift_unit.map residueMap.mapMatrix).unit
128   obtain ⟨P, hP, hi⟩ := exists_isomorphism_lift residueMap residue_surjective
129     rho tau group_order_unit B (by simpa only [B, IsUnit.unit_spec, RingHom.mapMatrix_apply] using residual_intertwining)
130   exact ⟨P, by simpa only [B, IsUnit.unit_spec, RingHom.mapMatrix_apply] using hP, hi⟩
131 
132 noncomputable abbrev threeIdeal : Ideal ℤ_[3] := IsLocalRing.maximalIdeal ℤ_[3]
133 
134 /-- A unit comparison gives the fixed detecting depth one. -/
135 theorem averaged_depth_one : Ideal.Quotient.mk (threeIdeal^1) averagedComparison.det ≠ 0 := by
136   have hdet := (Matrix.isUnit_iff_isUnit_det _).mp averaged_isUnit
137   rw [pow_one]
138   exact (hdet.map (Ideal.Quotient.mk threeIdeal)).ne_zero
139 
140 /-- Concrete finite conditions, populated by the displayed framed representation. -/
141 noncomputable def fixedConditions : Conditions (G := C2) (ι := Fin 2) threeIdeal where
142   allowed k σ := σ = reduce threeIdeal rho k
143   downward := by
144     intro j k hjk σ hσ
145     rw [hσ]
146     exact transition_reduce threeIdeal rho hjk
147 
148 theorem fixed_residual_type :
149     AveragingCompletion.ResidualType threeIdeal fixedConditions tau := by
150   intro σ hσ
151   change σ = reduce threeIdeal rho 1 at hσ
152   subst σ
153   let P := averaged_isUnit.unit
154   let f := Ideal.Quotient.mk (threeIdeal^1)
155   refine ⟨Units.map f.mapMatrix.toMonoidHom P, ?_⟩
156   intro g
157   have hi := congrArg (fun M => f.mapMatrix M) (averaged_intertwining g)
158   change (rho g).map f * (P : Matrix (Fin 2) (Fin 2) ℤ_[3]).map f =
159     (P : Matrix (Fin 2) (Fin 2) ℤ_[3]).map f * (tau g).map f
160   rw [show (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) = averagedComparison from averaged_isUnit.unit_spec]
161   exact hi
162 
163 /-- The new completion theorem is genuinely invoked. In this explicit example
164 the displayed rho supplies occupancy; no new global occupancy claim is made. -/
165 theorem actual_three_adic_averaging_completion :
166     ∃ (σ : MatrixRep ℤ_[3] C2 (Fin 2)) (P : (Matrix (Fin 2) (Fin 2) ℤ_[3])ˣ),
167       Realizes threeIdeal fixedConditions σ ∧ AdicRepContinuous threeIdeal σ ∧
168       (∀ g, σ g * (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) =
169         (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) * tau g) ∧
170       Ideal.Quotient.mk (threeIdeal^1) (P : Matrix (Fin 2) (Fin 2) ℤ_[3]).det ≠ 0 := by
171   apply AveragingCompletion.continuous_finite_group_completion threeIdeal fixedConditions
172     (IsLocalRing.maximalIdeal.isMaximal ℤ_[3]).ne_top tau group_order_unit fixed_residual_type
173   · intro k
174     exact Ideal.finite_quotient_pow (IsNoetherian.noetherian threeIdeal) k
175   · intro k
176     exact ⟨reduce threeIdeal rho k, rfl⟩
177 
178 noncomputable def galoisRho : MatrixRep ℤ_[3] ArithmeticCertificateExample.GQ (Fin 2) :=
179   rho.comp ArithmeticCertificateExample.quadraticCharacter
180 
181 noncomputable def galoisTau : MatrixRep ℤ_[3] ArithmeticCertificateExample.GQ (Fin 2) :=
182   tau.comp ArithmeticCertificateExample.quadraticCharacter
183 
184 theorem galois_rho_continuous : AdicRepContinuous threeIdeal galoisRho := by
185   let : TopologicalSpace ℤ_[3] := threeIdeal.adicTopology
186   exact (continuous_of_discreteTopology (f := rho)).comp
187     ArithmeticCertificateExample.quadraticCharacter_continuous
188 
189 theorem galois_tau_continuous : AdicRepContinuous threeIdeal galoisTau := by
190   let : TopologicalSpace ℤ_[3] := threeIdeal.adicTopology
191   exact (continuous_of_discreteTopology (f := tau)).comp
192     ArithmeticCertificateExample.quadraticCharacter_continuous
193 
194 /-- Averaging on the finite quotient gives an actual integral isomorphism of
195 continuous representations of the absolute Galois group of Q. -/
196 theorem actual_galois_integral_isomorphism :
197     ∃ P : (Matrix (Fin 2) (Fin 2) ℤ_[3])ˣ,
198       (P : Matrix (Fin 2) (Fin 2) ℤ_[3]).map residueMap = initialLift.map residueMap ∧
199       ∀ g, galoisRho g * (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) =
200         (P : Matrix (Fin 2) (Fin 2) ℤ_[3]) * galoisTau g := by
201   obtain ⟨P, hp, hi⟩ := actual_three_adic_isomorphism_lift
202   exact ⟨P, hp, fun g => hi (ArithmeticCertificateExample.quadraticCharacter g)⟩
203 
204 /-- The arithmetic source does act nontrivially; this is not a trivial-group
205 specialization disguised by its name. -/
206 theorem actual_galois_generator_values :
207     ∃ g : ArithmeticCertificateExample.GQ,
208       galoisRho g = !![1, 1; 0, -1] ∧ galoisTau g = !![1, 0; 0, -1] := by
209   obtain ⟨g, hg⟩ := ArithmeticCertificateExample.quadraticCharacter_hits_generator
210   refine ⟨g, ?_, ?_⟩ <;> ext i j <;> fin_cases i <;> fin_cases j <;>
211     norm_num [galoisRho, galoisTau, MonoidHom.comp_apply, hg, rho, tau,
212       changeCoefficients, integerRho, signRep, signValue, generator, Matrix.map]
213 
214 end PaperX.AveragingExamples

Back to source controls