ArithmeticCertificateExample.lean

1 import PaperX.CompletionExamples
2 import Mathlib.FieldTheory.AbsoluteGaloisGroup
3 import Mathlib.FieldTheory.Galois.Infinite
4 import PaperX.CertificateIsomorphisms
5 
6 /-! A concrete quadratic character of the actual absolute Galois group of Q,
7 defined by its action on a square root of minus one in the algebraic closure. -/
8 set_option autoImplicit false
9 namespace PaperX.ArithmeticCertificateExample
10 open PaperX.CompletionExamples PaperX.RepresentationLimits
11 open PaperX.RepresentationTopology PaperX.RepresentationClasses
12 open scoped Matrix
13 open scoped Topology
14 
15 abbrev Qbar := AlgebraicClosure ℚ
16 /-- This is definitionally `Field.absoluteGaloisGroup ℚ`, with its Krull topology. -/
17 abbrev GQ := Qbar ≃ₐ[ℚ] Qbar
18 
19 noncomputable def imaginary : Qbar :=
20   Classical.choose (IsAlgClosed.exists_pow_nat_eq (-1 : Qbar) (by decide : 0 < 2))
21 
22 theorem imaginary_sq : imaginary ^ 2 = -1 :=
23   Classical.choose_spec (IsAlgClosed.exists_pow_nat_eq (-1 : Qbar) (by decide : 0 < 2))
24 
25 theorem imaginary_ne_zero : imaginary ≠ 0 := by
26   intro h
27   have := imaginary_sq
28   rw [h] at this
29   norm_num at this
30 
31 theorem imaginary_ne_neg : imaginary ≠ -imaginary := by
32   intro h
33   have : (2 : Qbar) * imaginary = 0 := by linear_combination h
34   exact imaginary_ne_zero ((mul_eq_zero.mp this).resolve_left (by norm_num))
35 
36 theorem imaginary_not_rational : imaginary ∉ Set.range (algebraMap ℚ Qbar) := by
37   rintro ⟨q, hq⟩
38   have h : (algebraMap ℚ Qbar) (q ^ 2) = (algebraMap ℚ Qbar) (-1) := by
39     simpa [map_pow, hq] using imaginary_sq
40   have hq2 : q ^ 2 = -1 := (algebraMap ℚ Qbar).injective h
41   nlinarith [sq_nonneg q]
42 
43 theorem action_imaginary (σ : GQ) : σ imaginary = imaginary ∨ σ imaginary = -imaginary := by
44   have hs : (σ imaginary) ^ 2 = imaginary ^ 2 := by
45     rw [← map_pow, imaginary_sq, map_neg, map_one]
46   exact sq_eq_sq_iff_eq_or_eq_neg.mp hs
47 
48 noncomputable def quadraticValue (σ : GQ) : C2 := by
49   classical
50   exact if σ imaginary = imaginary then 1 else generator
51 
52 theorem quadraticValue_mul (σ τ : GQ) :
53     quadraticValue (σ * τ) = quadraticValue σ * quadraticValue τ := by
54   have hgen : generator * generator = 1 := by decide +kernel
55   by_cases hs : σ imaginary = imaginary
56   · by_cases ht : τ imaginary = imaginary
57     · have hst : (σ * τ) imaginary = imaginary := by
58         change σ (τ imaginary) = imaginary
59         rw [ht, hs]
60       simp only [quadraticValue, ite_eq_left hst, ite_eq_left hs, ite_eq_left ht, mul_one]
61     · have ht' : τ imaginary = -imaginary := (action_imaginary τ).resolve_left ht
62       have hst : (σ * τ) imaginary ≠ imaginary := by
63         change σ (τ imaginary) ≠ imaginary
64         rw [ht', map_neg, hs]
65         exact imaginary_ne_neg.symm
66       simp only [quadraticValue, ite_eq_right hst, ite_eq_left hs, ite_eq_right ht, one_mul]
67   · have hs' : σ imaginary = -imaginary := (action_imaginary σ).resolve_left hs
68     by_cases ht : τ imaginary = imaginary
69     · have hst : (σ * τ) imaginary ≠ imaginary := by
70         change σ (τ imaginary) ≠ imaginary
71         rw [ht]
72         exact hs
73       simp only [quadraticValue, ite_eq_right hst, ite_eq_right hs, ite_eq_left ht, mul_one]
74     · have ht' : τ imaginary = -imaginary := (action_imaginary τ).resolve_left ht
75       have hst : (σ * τ) imaginary = imaginary := by
76         change σ (τ imaginary) = imaginary
77         rw [ht', map_neg, hs', neg_neg]
78       simp only [quadraticValue, ite_eq_left hst, ite_eq_right hs, ite_eq_right ht, hgen]
79 
80 noncomputable def quadraticCharacter : GQ →* C2 where
81   toFun := quadraticValue
82   map_one' := by simp [quadraticValue]
83   map_mul' := quadraticValue_mul
84 
85 theorem quadraticCharacter_hits_generator : ∃ σ : GQ, quadraticCharacter σ = generator := by
86   have h : ¬ ∀ σ : GQ, σ imaginary = imaginary := by
87     intro h
88     exact imaginary_not_rational
89       ((InfiniteGalois.mem_range_algebraMap_iff_fixed imaginary).mpr h)
90   obtain ⟨σ, hσ⟩ := Classical.not_forall.mp h
91   exact ⟨σ, by simp [quadraticCharacter, quadraticValue, hσ]⟩
92 
93 theorem quadraticCharacter_continuous : Continuous quadraticCharacter := by
94   apply continuous_of_continuousAt_one quadraticCharacter
95   rw [ContinuousAt, nhds_discrete C2, Filter.tendsto_pure]
96   have hopen : IsOpen {σ : GQ | σ imaginary = imaginary} := by
97     exact stabilizer_isOpen_of_isIntegral imaginary
98   filter_upwards [hopen.mem_nhds (show (1 : GQ) imaginary = imaginary from rfl)] with σ hσ
99   simp [quadraticCharacter, quadraticValue, hσ]
100 
101 /-- The character also has the explicitly named absolute Galois group as domain. -/
102 noncomputable def absoluteQuadraticCharacter : Field.absoluteGaloisGroup ℚ →* C2 :=
103   quadraticCharacter
104 
105 theorem absoluteQuadraticCharacter_continuous : Continuous absoluteQuadraticCharacter :=
106   quadraticCharacter_continuous
107 
108 /-- An integral lattice representation with the same rational constituents as
109 the diagonal sign representation, but a different reduction modulo two. -/
110 def nonsplitRep : MatrixRep ℤ C2 (Fin 2) where
111   toFun g := if g.toAdd = 0 then 1 else !![1, -1; 0, -1]
112   map_one' := by decide +kernel
113   map_mul' := by decide +kernel
114 
115 def integralComparison : Matrix (Fin 2) (Fin 2) ℤ := !![1, 1; 0, 2]
116 
117 theorem integral_comparison_det : integralComparison.det = 2 := by decide +kernel
118 
119 theorem integral_intertwining : ∀ g : C2,
120     nonsplitRep g * integralComparison = integralComparison * signRep g := by
121   decide +kernel
122 
123 instance twoPrime : Fact (Nat.Prime 2) := ⟨by decide⟩
124 
125 noncomputable abbrev twoIdeal : Ideal ℤ_[2] := IsLocalRing.maximalIdeal ℤ_[2]
126 
127 noncomputable def tau : MatrixRep ℤ_[2] GQ (Fin 2) :=
128   (changeCoefficients (Int.castRingHom ℤ_[2]) signRep).comp quadraticCharacter
129 
130 noncomputable def rho : MatrixRep ℤ_[2] GQ (Fin 2) :=
131   (changeCoefficients (Int.castRingHom ℤ_[2]) nonsplitRep).comp quadraticCharacter
132 
133 noncomputable def comparison : Matrix (Fin 2) (Fin 2) ℤ_[2] :=
134   integralComparison.map (Int.castRingHom ℤ_[2])
135 
136 theorem comparison_det : comparison.det = 2 := by
137   change ((Int.castRingHom ℤ_[2]).mapMatrix integralComparison).det = 2
138   rw [← RingHom.map_det, integral_comparison_det, map_ofNat]
139 
140 theorem comparison_intertwining (g : GQ) : rho g * comparison = comparison * tau g := by
141   have h := congrArg (fun M => M.map (Int.castRingHom ℤ_[2]))
142     (integral_intertwining (quadraticCharacter g))
143   rw [Matrix.map_mul, Matrix.map_mul] at h
144   simpa [rho, tau, comparison, changeCoefficients] using h
145 
146 theorem tau_continuous : AdicRepContinuous twoIdeal tau := by
147   let : TopologicalSpace ℤ_[2] := twoIdeal.adicTopology
148   exact (continuous_of_discreteTopology (f :=
149     (changeCoefficients (Int.castRingHom ℤ_[2]) signRep))).comp
150     quadraticCharacter_continuous
151 
152 theorem rho_continuous : AdicRepContinuous twoIdeal rho := by
153   let : TopologicalSpace ℤ_[2] := twoIdeal.adicTopology
154   exact (continuous_of_discreteTopology (f :=
155     (changeCoefficients (Int.castRingHom ℤ_[2]) nonsplitRep))).comp
156     quadraticCharacter_continuous
157 
158 /-- The determinant is not zero modulo four even though it is not an integral unit. -/
159 theorem comparison_det_mod_four : PadicInt.toZModPow 2 comparison.det ≠ 0 := by
160   rw [comparison_det, map_ofNat]
161   decide +kernel
162 
163 theorem comparison_det_detected : Ideal.Quotient.mk (twoIdeal ^ 2) comparison.det ≠ 0 := by
164   intro hz
165   have hm := Ideal.Quotient.eq_zero_iff_mem.mp hz
166   rw [show twoIdeal = Ideal.span {(2 : ℤ_[2])} from
167     PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow] at hm
168   apply comparison_det_mod_four
169   change comparison.det ∈ RingHom.ker (PadicInt.toZModPow 2)
170   rw [PadicInt.ker_toZModPow]
171   exact hm
172 
173 theorem comparison_not_unit : ¬ IsUnit comparison := by
174   intro hu
175   have hd := (Matrix.isUnit_iff_isUnit_det comparison).mp hu
176   rw [comparison_det] at hd
177   have hf := hd.map (PadicInt.toZMod : ℤ_[2] →+* ZMod 2)
178   simp only [map_ofNat] at hf
179   rw [show (2 : ZMod 2) = 0 by decide +kernel] at hf
180   exact not_isUnit_zero hf
181 
182 /-- A genuine isomorphism over Q_2 follows from the fixed finite determinant
183 certificate, for representations of the actual absolute Galois group. -/
184 theorem field_conjugacy :
185     Conjugate (changeCoefficients (algebraMap ℤ_[2] ℚ_[2]) tau)
186       (changeCoefficients (algebraMap ℤ_[2] ℚ_[2]) rho) := by
187   apply PaperX.CertificateIsomorphisms.conjugate_of_finite_certificate twoIdeal
188     (algebraMap ℤ_[2] ℚ_[2]) (fun _ _ h => Subtype.ext h) rho tau comparison 2
189   · change ((Ideal.Quotient.mk (twoIdeal ^ 2)).mapMatrix comparison).det ≠ 0
190     rw [← RingHom.map_det]
191     exact comparison_det_detected
192   · exact comparison_intertwining
193 
194 theorem tau_residue (g : GQ) :
195     changeCoefficients (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) tau g = 1 := by
196   have h : ∀ c : C2, (signRep c).map (Int.castRingHom (ZMod 2)) = 1 := by
197     decide +kernel
198   ext i j
199   have H := congrArg (fun M => M i j) (h (quadraticCharacter g))
200   simpa [tau, changeCoefficients] using H
201 
202 theorem rho_residue_generator (g : GQ) (hg : quadraticCharacter g = generator) :
203     changeCoefficients (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) rho g 0 1 = 1 := by
204   norm_num [rho, changeCoefficients, hg, nonsplitRep, generator]
205 
206 /-- No integral change of basis works: a genuine Galois element has trivial
207 tau reduction but a nonidentity rho reduction modulo two. -/
208 theorem not_integrally_conjugate : ¬ Conjugate tau rho := by
209   intro hc
210   obtain ⟨g, hg⟩ := quadraticCharacter_hits_generator
211   obtain ⟨u, hu⟩ := changeCoefficients_conjugacy
212     (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) hc
213   have H := congrArg (fun σ : MatrixRep (ZMod 2) GQ (Fin 2) => σ g) hu
214   rw [conjugate_apply, tau_residue] at H
215   have H01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 2) => M 0 1) H
216   simp at H01
217   have H1 := rho_residue_generator g hg
218   exact zero_ne_one (H01.trans H1)
219 
220 end PaperX.ArithmeticCertificateExample

Back to source controls