UnramifiedFieldTower.lean

1 import PaperXI.UnramifiedBaseChangeFactor
2 import Mathlib.RingTheory.Finiteness.Basic
3 import Mathlib.LinearAlgebra.Dimension.Free
4 
5 /-! # Recursive unramified local-field towers
6 
7 This module constructs the upper field over the already constructed lower field,
8 using the checked residue-field equivalence to transport a finite residue tower.
9 The resulting map on the integer-degree unramified Weil models is defined by the
10 actual relative residue degree.  No absolute Weil group is asserted.
11 -/
12 
13 set_option autoImplicit false
14 noncomputable section
15 
16 namespace PaperXI.UnramifiedFieldTower
17 
18 open PaperXI.LocalFieldResidueExtension
19 open PaperXI.IntegerRingComparison
20 open PaperXI.FiniteUnramifiedWeil
21 open PaperXI.ResidueDegreeBaseChange
22 open ValuativeRel
23 open scoped Classical
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 variable (t : Type*) [Field t] [Algebra s t] [FiniteDimensional s t]
30 
31 /-- The first spectral unramified extension in the tower. -/
32 abbrev LowerField := LocalFieldResidueExtension.field K s
33 
34 /-- Transport the residue algebra structure on `t` across the checked
35 residue-field equivalence `𝓀[LowerField] ≃ s`. -/
36 noncomputable def residueTowerMap : 𝓀[LowerField K s] →+* t :=
37   (algebraMap s t).comp (spectralResidueAlgEquiv K s).toRingHom
38 
39 noncomputable local instance residueTowerAlgebra : Algebra 𝓀[LowerField K s] t :=
40   (residueTowerMap K s t).toAlgebra
41 
42 noncomputable local instance residueTowerFinite :
43     FiniteDimensional 𝓀[LowerField K s] t := by
44   let e₁ : s ≃+* 𝓀[LowerField K s] :=
45     (spectralResidueAlgEquiv K s).symm.toRingEquiv
46   let e₂ : t ≃+* t := RingEquiv.refl t
47   exact Module.Finite.of_equiv_equiv e₁ e₂ (by
48     ext x
49     simp [e₁, e₂, residueTowerMap, RingHom.algebraMap_toAlgebra])
50 
51 /-- The second spectral unramified extension, now constructed over the actual
52 first local field rather than directly over the original base. -/
53 abbrev UpperField := LocalFieldResidueExtension.field (LowerField K s) t
54 
55 
56 
57 /-- The original base acts on the recursively constructed upper field through
58 the actual two-step field tower. -/
59 noncomputable local instance upperBaseAlgebra : Algebra K (UpperField K s t) :=
60   ((algebraMap (LowerField K s) (UpperField K s t)).comp
61     (algebraMap K (LowerField K s))).toAlgebra
62 
63 noncomputable local instance upperBaseTower :
64     IsScalarTower K (LowerField K s) (UpperField K s t) :=
65   IsScalarTower.of_algebraMap_eq fun _ => rfl
66 
67 /-- The actual inclusion of the lower local field into the recursive upper
68 local field, viewed over the original base. -/
69 noncomputable def lowerToUpper :
70     LowerField K s →ₐ[K] UpperField K s t :=
71   IsScalarTower.toAlgHom K (LowerField K s) (UpperField K s t)
72 
73 omit [FiniteDimensional s t] in
74 /-- The transported residue degree is the original degree `[t:s]`. -/
75 theorem residue_finrank :
76     Module.finrank 𝓀[LowerField K s] t = Module.finrank s t := by
77   apply Algebra.finrank_eq_of_equiv_equiv
78     (spectralResidueAlgEquiv K s).toRingEquiv (RingEquiv.refl t)
79   ext x
80   simp [residueTowerMap, RingHom.algebraMap_toAlgebra]
81 
82 /-- The actual relative degree of the recursive local-field extension. -/
83 theorem relative_degree :
84     Module.finrank (LowerField K s) (UpperField K s t) = Module.finrank s t := by
85   rw [LocalFieldResidueExtension.degree]
86   exact residue_finrank K s t
87 
88 
89 /-- The total degree is the product of the two actual residue degrees. -/
90 theorem total_degree :
91     Module.finrank K (UpperField K s t) =
92       Module.finrank 𝓀[K] s * Module.finrank s t := by
93   rw [← Module.finrank_mul_finrank K (LowerField K s) (UpperField K s t),
94     LocalFieldResidueExtension.degree K s, relative_degree K s t]
95 
96 /-- The residue field of the recursive upper local field is the declared top
97 finite field. -/
98 noncomputable def upperResidueAlgEquiv :
99     𝓀[UpperField K s t] ≃ₐ[𝓀[LowerField K s]] t :=
100   spectralResidueAlgEquiv (LowerField K s) t
101 
102 /-- The recursive upper extension is unramified at the level of spectral
103 integer rings. -/
104 theorem relative_ramificationIdx_one :
105     (IsLocalRing.maximalIdeal 𝒪[UpperField K s t]).ramificationIdx
106       𝒪[LowerField K s] = 1 :=
107   spectral_ramificationIdx_one (LowerField K s) t
108 
109 /-- Restriction on the current integer-degree unramified Weil models.  In degree
110 coordinates it is multiplication by the actual relative field degree. -/
111 noncomputable def restriction :
112     UnramifiedWeil (LowerField K s) t →* UnramifiedWeil K s :=
113   (degreeEquiv K s).symm.toMonoidHom.comp
114     ((integerDegreeDilation (Module.finrank s t)).comp
115       (degreeEquiv (LowerField K s) t).toMonoidHom)
116 
117 
118 /-- In canonical degree coordinates, field-tower restriction is literally the
119 Block 40 integer-degree dilation. -/
120 theorem restriction_degree_square :
121     (degreeEquiv K s).toMonoidHom.comp (restriction K s t) =
122       (integerDegreeDilation (Module.finrank s t)).comp
123         (degreeEquiv (LowerField K s) t).toMonoidHom :=
124   rfl
125 
126 @[simp]
127 theorem restriction_degree (w : UnramifiedWeil (LowerField K s) t) :
128     Multiplicative.toAdd (degreeEquiv K s (restriction K s t w)) =
129       (Module.finrank s t : ℤ) *
130         Multiplicative.toAdd (degreeEquiv (LowerField K s) t w) := by
131   simp [restriction, integerDegreeDilation]
132 
133 /-- Upper geometric Frobenius restricts to the relative-degree power of lower
134 geometric Frobenius. -/
135 @[simp]
136 theorem restriction_geometricLift :
137     restriction K s t (geometricLift (LowerField K s) t) =
138       geometricLift K s ^ (Module.finrank s t : ℕ) := by
139   apply (degreeEquiv K s).injective
140   apply Multiplicative.toAdd.injective
141   calc
142     Multiplicative.toAdd
143         (degreeEquiv K s
144           (restriction K s t (geometricLift (LowerField K s) t))) =
145         (Module.finrank s t : ℤ) *
146           Multiplicative.toAdd
147             (degreeEquiv (LowerField K s) t
148               (geometricLift (LowerField K s) t)) :=
149       restriction_degree K s t _
150     _ = (Module.finrank s t : ℤ) := by
151       rw [degreeEquiv_apply, degree_geometricLift]
152       simp
153     _ = Multiplicative.toAdd
154         (degreeEquiv K s (geometricLift K s ^ Module.finrank s t)) := by
155       rw [map_pow, degreeEquiv_apply, degree_geometricLift]
156       simp
157 
158 /-- The restriction map is injective. -/
159 theorem restriction_injective : Function.Injective (restriction K s t) := by
160   intro a b h
161   apply (degreeEquiv (LowerField K s) t).injective
162   apply Multiplicative.toAdd.injective
163   have hf_nat : Module.finrank s t ≠ 0 := Module.finrank_pos.ne'
164   have hf : (Module.finrank s t : ℤ) ≠ 0 := by
165     exact_mod_cast hf_nat
166   have hdeg :
167       (Module.finrank s t : ℤ) *
168           Multiplicative.toAdd (degreeEquiv (LowerField K s) t a) =
169         (Module.finrank s t : ℤ) *
170           Multiplicative.toAdd (degreeEquiv (LowerField K s) t b) := by
171     calc
172       (Module.finrank s t : ℤ) *
173           Multiplicative.toAdd (degreeEquiv (LowerField K s) t a) =
174         Multiplicative.toAdd (degreeEquiv K s (restriction K s t a)) :=
175           (restriction_degree K s t a).symm
176       _ = Multiplicative.toAdd (degreeEquiv K s (restriction K s t b)) :=
177         congrArg (fun w : UnramifiedWeil K s =>
178           Multiplicative.toAdd (degreeEquiv K s w)) h
179       _ = (Module.finrank s t : ℤ) *
180           Multiplicative.toAdd (degreeEquiv (LowerField K s) t b) :=
181         restriction_degree K s t b
182   exact mul_left_cancel₀ hf hdeg
183 
184 
185 /-- The image is exactly the subgroup whose lower integer degrees are divisible
186 by the actual relative residue degree. -/
187 theorem restriction_range :
188     (restriction K s t).range =
189       periodSubgroup (MonoidHom.id (ResidueGalois K s))
190         (geometricFrobenius K s) (Module.finrank s t) := by
191   ext w
192   constructor
193   · rintro ⟨v, rfl⟩
194     rw [mem_periodSubgroup]
195     rw [← degreeEquiv_apply]
196     rw [restriction_degree]
197     exact dvd_mul_right _ _
198   · intro hw
199     have hd : (Module.finrank s t : ℤ) ∣
200         Multiplicative.toAdd (degreeEquiv K s w) := by
201       simpa only [degreeEquiv_apply] using
202         (mem_periodSubgroup _ _ _ w).mp hw
203     obtain ⟨m, hm⟩ := hd
204     let v : UnramifiedWeil (LowerField K s) t :=
205       (degreeEquiv (LowerField K s) t).symm (Multiplicative.ofAdd m)
206     refine ⟨v, ?_⟩
207     apply (degreeEquiv K s).injective
208     apply Multiplicative.toAdd.injective
209     rw [restriction_degree]
210     have hv : Multiplicative.toAdd
211         (degreeEquiv (LowerField K s) t v) = m := by
212       simp [v]
213     rw [hv]
214     simpa only [degreeEquiv_apply] using hm.symm
215 
216 /-- Restriction is an equivalence onto the exact degree-period subgroup. -/
217 noncomputable def restrictionEquivPeriod :
218     UnramifiedWeil (LowerField K s) t ≃*
219       periodSubgroup (MonoidHom.id (ResidueGalois K s))
220         (geometricFrobenius K s) (Module.finrank s t) :=
221   (MonoidHom.ofInjective (restriction_injective K s t)).trans
222     (MulEquiv.subgroupCongr (restriction_range K s t))
223 
224 /-- Any homomorphism between the same current Weil models with the genuine
225 relative-degree formula is the restriction map constructed above.  This is the
226 uniqueness principle used to reconcile older Henselian tower embeddings with
227 the newer spectral models. -/
228 theorem restriction_unique
229     (φ : UnramifiedWeil (LowerField K s) t →* UnramifiedWeil K s)
230     (hφ : ∀ w, Multiplicative.toAdd (degreeEquiv K s (φ w)) =
231       (Module.finrank s t : ℤ) *
232         Multiplicative.toAdd (degreeEquiv (LowerField K s) t w)) :
233     φ = restriction K s t := by
234   apply MonoidHom.ext
235   intro w
236   apply (degreeEquiv K s).injective
237   apply Multiplicative.toAdd.injective
238   exact (hφ w).trans (restriction_degree K s t w).symm
239 
240 
241 section Representation
242 
243 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
244 
245 /-- Restriction of a representation along the actual recursive field-tower map. -/
246 def restrictRepresentation
247     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
248     Representation ℂ (UnramifiedWeil (LowerField K s) t) V :=
249   ρ.comp (restriction K s t)
250 
251 omit [FiniteDimensional ℂ V] in
252 @[simp]
253 theorem restrictRepresentation_geometricLift
254     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
255     restrictRepresentation K s t ρ (geometricLift (LowerField K s) t) =
256       ρ (geometricLift K s ^ Module.finrank s t) := by
257   simp [restrictRepresentation]
258 
259 /-- The Frobenius polynomial after actual tower restriction is the reverse
260 characteristic polynomial of the relative-degree Frobenius power. -/
261 theorem restriction_frobeniusPolynomial
262     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
263     frobeniusPolynomial (LowerField K s) t (restrictRepresentation K s t ρ) =
264       (LinearMap.charpoly
265         (ρ (geometricLift K s ^ Module.finrank s t))).reverse := by
266   rw [frobeniusPolynomial, restrictRepresentation_geometricLift]
267 
268 end Representation
269 
270 end PaperXI.UnramifiedFieldTower

Back to source controls