IntegerRingComparison.lean

1 import PaperXI.SpectralLocalField
2 import Mathlib.RingTheory.Polynomial.Subring
3 import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
4 
5 /-!
6 # Comparison of the algebraic and spectral integer rings
7 
8 For the unramified residue extension constructed in `LocalFieldResidueExtension`,
9 the finite-extension spectral norm has unit ball equal to the image of the
10 algebraically constructed complete DVR.  The proof proceeds through the exact
11 integrality criterion over the base local-field integers.
12 -/
13 
14 set_option autoImplicit false
15 noncomputable section
16 
17 namespace PaperXI.IntegerRingComparison
18 
19 open PaperXI.LocalFieldResidueExtension
20 open PaperXI.CanonicalDVRValuation
21 open PaperXI.SpectralLocalField
22 open ValuativeRel
23 open scoped WithZero Polynomial
24 
25 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
26   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
27 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
28   [FiniteDimensional 𝓀[K] s]
29 
30 private local instance baseValued : Valued K (ValueGroupWithZero K) := inferInstance
31 
32 private local instance baseRankOne :
33     Valuation.RankOne (Valued.v (R := K) (Γ₀ := ValueGroupWithZero K)) :=
34   { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp
35       MonoidWithZeroHom.ValueGroup₀.embedding
36     strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
37       MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
38 
39 private local instance baseNormedField : NormedField K :=
40   Valued.toNormedField K (ValueGroupWithZero K)
41 
42 private local instance baseNontriviallyNormedField : NontriviallyNormedField K :=
43   Valued.toNontriviallyNormedField K (ValueGroupWithZero K)
44 
45 abbrev UpperRing := LocalFieldResidueExtension.ring K s
46 abbrev UpperField := LocalFieldResidueExtension.field K s
47 
48 /-- Spectral integrality is exactly algebraic integrality over the base local
49 field integers. -/
50 theorem norm_le_one_iff_isIntegral (x : UpperField K s) :
51     ‖x‖ ≤ 1 ↔ IsIntegral 𝒪[K] x := by
52   constructor
53   · intro hx
54     have hxalg : IsIntegral K x := Algebra.IsIntegral.isIntegral x
55     have hmonic : (minpoly K x).Monic := minpoly.monic hxalg
56     have hcoeffNorm : ∀ n : ℕ, ‖(minpoly K x).coeff n‖ ≤ 1 := by
57       have hspectral : spectralNorm K (UpperField K s) x ≤ 1 := by
58         simpa [SpectralLocalField.norm_eq_spectralNorm] using hx
59       exact (spectralValue_le_one_iff hmonic).mp hspectral
60     have hcoeff : (↑(minpoly K x).coeffs : Set K) ⊆ (𝒪[K] : Set K) := by
61       intro c hc
62       rw [Finset.mem_coe, Polynomial.mem_coeffs_iff] at hc
63       obtain ⟨n, -, rfl⟩ := hc
64       have hv : Valued.v ((minpoly K x).coeff n) ≤ 1 :=
65         (Valued.toNormedField.norm_le_one_iff).mp (hcoeffNorm n)
66       change (ValuativeRel.valuation K) ((minpoly K x).coeff n) ≤ 1
67       exact hv
68     let p : Polynomial 𝒪[K] := Polynomial.toSubring (minpoly K x) 𝒪[K] hcoeff
69     have hpmonic : p.Monic :=
70       (Polynomial.monic_toSubring (minpoly K x) 𝒪[K] hcoeff).2 hmonic
71     have hpmapSubtype : p.map (Subring.subtype 𝒪[K]) = minpoly K x := by
72       dsimp [p]
73       exact Polynomial.map_toSubring (minpoly K x) 𝒪[K] hcoeff
74     have hpmap : p.map (algebraMap 𝒪[K] K) = minpoly K x := by
75       rw [Algebra.algebraMap_ofSubring]
76       exact hpmapSubtype
77     have hpeval : Polynomial.aeval x p = 0 := by
78       rw [← Polynomial.aeval_map_algebraMap K x p, hpmap]
79       exact minpoly.aeval K x
80     exact ⟨p, hpmonic, hpeval⟩
81   · intro hx
82     have hxalg : IsIntegral K x := Algebra.IsIntegral.isIntegral x
83     rw [SpectralLocalField.norm_eq_spectralNorm, spectralNorm,
84       spectralValue_le_one_iff (minpoly.monic hxalg)]
85     intro n
86     rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hx, Polynomial.coeff_map]
87     change ‖(((minpoly 𝒪[K] x).coeff n : 𝒪[K]) : K)‖ ≤ 1
88     rw [Valued.toNormedField.norm_le_one_iff]
89     change (ValuativeRel.valuation K) (((minpoly 𝒪[K] x).coeff n : 𝒪[K]) : K) ≤ 1
90     exact ((minpoly 𝒪[K] x).coeff n).property
91 
92 omit [IsUniformAddGroup K] in
93 /-- Algebraic integrality over the base integer ring is equivalent to coming
94 from the constructed upper DVR. -/
95 theorem isIntegral_iff_exists_upper_lift (x : UpperField K s) :
96     IsIntegral 𝒪[K] x ↔
97       ∃ c : UpperRing K s,
98         algebraMap (UpperRing K s) (UpperField K s) c = x := by
99   constructor
100   · intro hx
101     have hxC : IsIntegral (UpperRing K s) x := hx.tower_top
102     exact IsIntegrallyClosedIn.isIntegral_iff.mp hxC
103   · rintro ⟨c, rfl⟩
104     exact (IsIntegral.of_finite 𝒪[K] c).algebraMap
105 
106 /-- Literal equality in the ambient fraction field between the algebraically
107 constructed DVR and the spectral local-field integer ring. -/
108 theorem upper_integerRing_eq_spectral :
109     Subring.map (algebraMap (UpperRing K s) (UpperField K s)) ⊤ =
110       𝒪[UpperField K s] := by
111   ext x
112   constructor
113   · rintro ⟨c, -, rfl⟩
114     exact (SpectralLocalField.mem_integer_iff_norm_le_one K s _).2 <|
115       (norm_le_one_iff_isIntegral K s _).2
116         ((IsIntegral.of_finite 𝒪[K] c).algebraMap)
117   · intro hx
118     have hnorm := (SpectralLocalField.mem_integer_iff_norm_le_one K s x).1 hx
119     obtain ⟨c, hc⟩ :=
120       (isIntegral_iff_exists_upper_lift K s x).1
121         ((norm_le_one_iff_isIntegral K s x).1 hnorm)
122     exact ⟨c, by simp, hc⟩
123 
124 
125 /-- The algebraically constructed upper DVR is canonically ring-equivalent to
126     the spectral local field's integer ring. -/
127 noncomputable def upperRingEquivSpectralIntegers :
128     UpperRing K s ≃+* 𝒪[UpperField K s] :=
129   (Subring.topEquiv : (⊤ : Subring (UpperRing K s)) ≃+* UpperRing K s).symm |>.trans
130     (((⊤ : Subring (UpperRing K s)).equivMapOfInjective
131       (algebraMap (UpperRing K s) (UpperField K s))
132       (FaithfulSMul.algebraMap_injective (UpperRing K s) (UpperField K s))).trans
133         (RingEquiv.subringCongr (upper_integerRing_eq_spectral K s)))
134 
135 /-- The base integer ring acts on the spectral integer ring through the checked
136     identification with the algebraic upper DVR. -/
137 noncomputable instance spectralIntegerAlgebra :
138     Algebra 𝒪[K] 𝒪[UpperField K s] :=
139   RingHom.toAlgebra
140     ((upperRingEquivSpectralIntegers K s).toRingHom.comp
141       (algebraMap 𝒪[K] (UpperRing K s)))
142 
143 noncomputable instance spectralIntegerAlgebra_isLocal :
144     IsLocalHom (algebraMap 𝒪[K] 𝒪[UpperField K s]) := by
145   change IsLocalHom
146     ((upperRingEquivSpectralIntegers K s).toRingHom.comp
147       (algebraMap 𝒪[K] (UpperRing K s)))
148   refine ⟨fun a ha => ?_⟩
149   have haUpper : IsUnit (algebraMap 𝒪[K] (UpperRing K s) a) :=
150     (isLocalHom_equiv (upperRingEquivSpectralIntegers K s)).map_nonunit _ ha
151   exact (inferInstance : IsLocalHom (algebraMap 𝒪[K] (UpperRing K s))).map_nonunit a haUpper
152 
153 /-- The integer-ring comparison is compatible with the original base integer
154     ring algebra structures. -/
155 noncomputable def upperRingAlgEquivSpectralIntegers :
156     UpperRing K s ≃ₐ[𝒪[K]] 𝒪[UpperField K s] :=
157   AlgEquiv.ofRingEquiv (f := upperRingEquivSpectralIntegers K s) (fun _ => rfl)
158 
159 noncomputable instance spectralIntegersEtale :
160     Algebra.Etale 𝒪[K] 𝒪[UpperField K s] := by
161   let _ : Algebra.Etale 𝒪[K] (UpperRing K s) :=
162     PaperXI.ResidueExtensionRealization.etale 𝒪[K] s
163   exact Algebra.Etale.of_equiv (upperRingAlgEquivSpectralIntegers K s)
164 
165 @[simp]
166 theorem upperRingEquivSpectralIntegers_coe (x : UpperRing K s) :
167     (((upperRingEquivSpectralIntegers K s x : 𝒪[UpperField K s]) :
168       UpperField K s)) = algebraMap (UpperRing K s) (UpperField K s) x := by
169   rfl
170 
171 /-- The integer-ring equivalence carries the algebraic maximal ideal to the
172     spectral local field's maximal ideal. -/
173 theorem upper_maximalIdeal_map :
174     Ideal.map (upperRingEquivSpectralIntegers K s).toRingHom
175       (IsLocalRing.maximalIdeal (UpperRing K s)) =
176         IsLocalRing.maximalIdeal 𝒪[UpperField K s] :=
177   IsLocalRing.map_ringEquiv_maximalIdeal
178     (upperRingEquivSpectralIntegers K s)
179 
180 /-- The spectral integer extension has ramification index one over the base
181     local-field integers. -/
182 theorem spectral_ramificationIdx_one :
183     (IsLocalRing.maximalIdeal 𝒪[UpperField K s]).ramificationIdx 𝒪[K] = 1 :=
184   Ideal.ramificationIdx_eq_one _ _
185 
186 /-- The residue field of the algebraic upper DVR is canonically ring-equivalent
187     to the residue field of the spectral local field. -/
188 noncomputable def upperResidueFieldEquivSpectral :
189     IsLocalRing.ResidueField (UpperRing K s) ≃+* 𝓀[UpperField K s] :=
190   IsLocalRing.ResidueField.mapEquiv (upperRingEquivSpectralIntegers K s)
191 
192 /-- The residue-field comparison respects the base residue field. -/
193 noncomputable def upperResidueFieldAlgEquivSpectral :
194     IsLocalRing.ResidueField (UpperRing K s) ≃ₐ[𝓀[K]] 𝓀[UpperField K s] :=
195   IsLocalRing.ResidueField.mapAlgEquiv'
196     (upperRingAlgEquivSpectralIntegers K s)
197 
198 /-- The spectral local field has the prescribed residue field as an algebra over
199     the original residue field. -/
200 noncomputable def spectralResidueAlgEquiv :
201     𝓀[UpperField K s] ≃ₐ[𝓀[K]] s :=
202   (upperResidueFieldAlgEquivSpectral K s).symm.trans
203     (PaperXI.ResidueExtensionRealization.residueEquiv 𝒪[K] s)
204 
205 /-- The spectral local field has the prescribed residue field, as an actual ring
206     equivalence. -/
207 noncomputable def spectralResidueEquiv :
208     𝓀[UpperField K s] ≃+* s :=
209   (upperResidueFieldEquivSpectral K s).symm.trans
210     (PaperXI.ResidueExtensionRealization.residueEquiv 𝒪[K] s).toRingEquiv
211 
212 /-- The spectral residue degree is exactly the prescribed residue-extension
213     degree. -/
214 theorem spectral_residue_finrank :
215     Module.finrank 𝓀[K] 𝓀[UpperField K s] = Module.finrank 𝓀[K] s :=
216   LinearEquiv.finrank_eq (spectralResidueAlgEquiv K s).toLinearEquiv
217 
218 /-- The field degree equals the spectral residue degree, the expected numerical
219     identity for the constructed unramified extension. -/
220 theorem upper_degree_eq_spectral_residue_finrank :
221     Module.finrank K (UpperField K s) = Module.finrank 𝓀[K] 𝓀[UpperField K s] := by
222   rw [LocalFieldResidueExtension.degree K s, spectral_residue_finrank K s]
223 
224 /-- Cardinality of the spectral residue field agrees with the prescribed finite
225     residue extension. -/
226 theorem natCard_spectralResidue :
227     Nat.card 𝓀[UpperField K s] = Nat.card s :=
228   Nat.card_congr (spectralResidueEquiv K s).toEquiv
229 
230 end PaperXI.IntegerRingComparison

Back to source controls