ActualMonomialLocalGlobal.lean

1 import PaperXI.FiniteTameComparison
2 import PaperXI.RamifiedUnramifiedQuotient
3 import PaperXI.ActualUnramifiedBaseChange
4 
5 /-!
6 # Actual tame-monomial attachment to the local-field ramification calculus
7 
8 The parameter in this file is constructed by genuine degree-subgroup induction
9 on the actual residue--Frobenius pullback.  Its finite packet invariants are
10 then attached to the literal lower ramification filtration and its conventional
11 Artin--Swan sums.  No automorphic representation, local class field theory, or
12 automorphic induction theorem is encoded as data in this Lean module.
13 -/
14 
15 set_option autoImplicit false
16 noncomputable section
17 
18 namespace PaperXI.ActualMonomialLocalGlobal
19 
20 open scoped Classical BigOperators Polynomial
21 open Polynomial
22 open PaperXI.ResidueWeil
23 open PaperXI.CyclicInduced
24 open PaperXI.TameOrbitTransitivity
25 open PaperXI.ValuationConductor
26 open PaperXI.ValuationRamification
27 open PaperXI.RamificationPolyphase
28 
29 section InvariantRange
30 
31 variable {G H V : Type*} [Group G] [Group H]
32 variable [AddCommGroup V] [Module ℂ V]
33 
34 /-- Invariant spaces depend only on the image of the acting homomorphism. -/
35 theorem invariants_eq_of_range_eq
36     (ρ : Representation ℂ G V) (f : H →* G) (S : Subgroup G)
37     (hrange : f.range = S) :
38     Representation.invariants (ρ.comp f) =
39       Representation.invariants (ρ.comp S.subtype) := by
40   ext v
41   constructor
42   · intro hv g
43     have hg : g.val ∈ f.range := by simpa [hrange] using g.property
44     obtain ⟨h, hh⟩ := hg
45     have hfix := hv h
46     change ρ (f h) v = v at hfix
47     simpa [hh] using hfix
48   · intro hv h
49     have hf : f h ∈ S := by
50       rw [← hrange]
51       exact ⟨h, rfl⟩
52     exact hv ⟨f h, hf⟩
53 
54 end InvariantRange
55 
56 section ActualTameParameter
57 
58 variable (R D : Type*) [CommRing R] [IsLocalRing R]
59   [Group D] [Fintype D] [MulSemiringAction D R]
60 variable (F : RingAut (IsLocalRing.ResidueField R))
61 
62 abbrev RamifiedWeil := Pullback (residue R D) F
63 abbrev actualDegree : RamifiedWeil R D F →* Multiplicative ℤ :=
64   degree (residue R D) F
65 
66 variable {M n : ℕ} [NeZero M] [NeZero n]
67 variable (ι : Multiplicative (ZMod M) →* RamifiedWeil R D F)
68 variable (hιrange : ι.range = (actualDegree R D F).ker)
69 variable (φ : RamifiedWeil R D F)
70 variable (hφ : actualDegree R D F φ = Multiplicative.ofAdd (1 : ℤ))
71 variable (ξ : TameDegree.degreeSubgroup (actualDegree R D F) n →* ℂˣ)
72 variable (q : (ZMod M)ˣ) (j : ZMod M)
73 variable (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
74   ι (Multiplicative.ofAdd (q : ZMod M)))
75 variable (hξ : ∀ a : ZMod M,
76   (ξ (InducedTameProfile.inertiaInDegree (actualDegree R D F) ι n
77     (Multiplicative.ofAdd a)) : ℂ) = ZMod.stdAddChar (j * a))
78 
79 /-- The actual monomial parameter is constructed by induction from the degree-
80 `n` subgroup of the literal residue--Frobenius pullback. -/
81 abbrev actualParameter : Representation ℂ (RamifiedWeil R D F)
82     (DegreeIndSpace (actualDegree R D F) n ξ) :=
83   degreeInduced (actualDegree R D F) n ξ
84 
85 /-- The finite cyclic inertia model is required to have exactly the same image
86 as the degree-zero inertia subgroup of the actual pullback. -/
87 theorem fixed_zero_eq_tame_invariants :
88     fixed R D F (actualParameter R D F n ξ) 0 =
89       (tameRestriction (actualParameter R D F n ξ) ι).invariants := by
90   rw [fixed_zero]
91   exact (invariants_eq_of_range_eq (actualParameter R D F n ξ) ι
92     (actualDegree R D F).ker hιrange).symm
93 
94 /-- The Block 43 projector is literally the projector onto the actual fixed
95 space of the constructed parameter. -/
96 theorem actual_depthProjector_range (i : ℕ) :
97     LinearMap.range (depthProjector (R := R) (D := D) (F := F)
98       (ρ := actualParameter R D F n ξ) i) =
99       fixed R D F (actualParameter R D F n ξ) i :=
100   depthProjector_range (R := R) (D := D) (F := F)
101     (ρ := actualParameter R D F n ξ) i
102 
103 /-- The actual ramification-detail channel is the newly fixed lower-depth
104 subspace with the preceding coarse component removed. -/
105 theorem actual_detailProjector_range (i : ℕ) :
106     LinearMap.range (detailProjector (R := R) (D := D) (F := F)
107       (ρ := actualParameter R D F n ξ) i) =
108       fixed R D F (actualParameter R D F n ξ) (i + 1) ⊓
109         LinearMap.ker (depthProjector (R := R) (D := D) (F := F)
110           (ρ := actualParameter R D F n ξ) i) :=
111   detailProjector_range (R := R) (D := D) (F := F)
112     (ρ := actualParameter R D F n ξ) i
113 
114 /-- Image of an actual lower ramification group in the ramified Weil pullback. -/
115 def lowerImage (i : ℕ) : Subgroup (RamifiedWeil R D F) :=
116   (lift R D F i).range
117 
118 /-- Rational form of the conventional lower-numbering weight. -/
119 def lowerWeight (i : ℕ) : ℚ :=
120   (Nat.card (lower R D i) : ℚ) / (Nat.card (lower R D 0) : ℚ)
121 
122 /-- Finite tame Swan expression formed from the actual lower-group images. -/
123 def packetSwan (S : Finset ℕ) : ℚ :=
124   TameConductor.finiteSwan (actualParameter R D F n ξ) S
125     (fun r => lowerImage R D F (r + 1))
126     (fun r => lowerWeight R D (r + 1))
127 
128 /-- Finite tame Artin expression formed from the actual inertia map and actual
129 lower-group images. -/
130 def packetArtin (S : Finset ℕ) : ℚ :=
131   TameConductor.finiteArtin (actualParameter R D F n ξ) ι S
132     (fun r => lowerImage R D F (r + 1))
133     (fun r => lowerWeight R D (r + 1))
134 
135 /-- The actual first lower group acts trivially in the declared tame class. -/
136 variable (htame : ∀ g : lower R D 1,
137   actualParameter R D F n ξ (lift R D F 1 g) = 1)
138 
139 include htame in
140 /-- Every positive lower-group image acts trivially. -/
141 theorem positive_lowerImage_trivial (r : ℕ) :
142     ∀ g ∈ lowerImage R D F (r + 1), ∀ v,
143       actualParameter R D F n ξ g v = v := by
144   intro g hg v
145   obtain ⟨h, rfl⟩ := hg
146   let h1 : lower R D 1 :=
147     RamificationPolyphase.lowerInclusion (R := R) (D := D)
148       (Nat.le_add_left 1 r) h
149   have hact := htame h1
150   have hlift : lift R D F 1 h1 = lift R D F (r + 1) h :=
151     RamificationPolyphase.lift_lowerInclusion (R := R) (D := D)
152       (F := F) (Nat.le_add_left 1 r) h
153   rw [hlift] at hact
154   exact LinearMap.congr_fun hact v
155 
156 include htame in
157 /-- The packet Swan expression vanishes because it uses the actual positive
158 lower-group images and those act trivially. -/
159 theorem packetSwan_eq_zero (S : Finset ℕ) :
160     packetSwan R D F n ξ S = 0 := by
161   unfold packetSwan TameConductor.finiteSwan
162   apply Finset.sum_eq_zero
163   intro r hr
164   rw [TameConductor.fixedCodimension_zero_of_trivial_on
165     (actualParameter R D F n ξ) (lowerImage R D F (r + 1))
166     (positive_lowerImage_trivial R D F n ξ htame r)]
167   simp
168 
169 include htame in
170 /-- The standard lower-numbering Swan conductor of the actual parameter
171 vanishes in the declared tame class. -/
172 theorem standardSwan_eq_zero :
173     swan R D F (actualParameter R D F n ξ) = 0 :=
174   tame_swan_zero R D F (actualParameter R D F n ξ) htame
175 
176 variable [FiniteDimensional ℂ (DegreeIndSpace (actualDegree R D F) n ξ)]
177 
178 include hφ hrel hξ htame in
179 /-- The conventional Artin conductor of the actual lower filtration is the
180 packet codimension: zero in the unramified label and `n` otherwise. -/
181 theorem standardArtin_eq_coordinates :
182     artin R D F (actualParameter R D F n ξ) =
183       if j = 0 then 0 else (n : ℝ) := by
184   unfold artin codimension
185   rw [standardSwan_eq_zero R D F n ξ htame, add_zero,
186     fixed_zero_eq_tame_invariants R D F ι hιrange n ξ,
187     InducedCycleInvariants.dimension (actualDegree R D F) φ hφ n ξ,
188     InducedTameProfile.invariant_dimension (actualDegree R D F) ι φ hφ n ξ
189       q j hrel hξ]
190   split_ifs <;> simp
191 
192 include hφ hrel hξ htame in
193 /-- The finite packet Artin expression built from the actual lower-group images
194 has the same coordinate value. -/
195 theorem packetArtin_eq_coordinates (S : Finset ℕ) :
196     packetArtin R D F ι n ξ S = if j = 0 then 0 else (n : ℚ) := by
197   unfold packetArtin TameConductor.finiteArtin
198   rw [packetSwan_eq_zero R D F n ξ htame S,
199     InducedCycleInvariants.dimension (actualDegree R D F) φ hφ n ξ,
200     InducedTameProfile.invariant_dimension (actualDegree R D F) ι φ hφ n ξ
201       q j hrel hξ]
202   split_ifs <;> simp
203 
204 include hφ hrel hξ htame in
205 /-- In the tame monomial class the finite packet expression is literally the
206 standard lower-numbering Artin conductor after scalar extension to `ℝ`. -/
207 theorem packetArtin_eq_standardArtin (S : Finset ℕ) :
208     ((packetArtin R D F ι n ξ S : ℚ) : ℝ) =
209       artin R D F (actualParameter R D F n ξ) := by
210   rw [packetArtin_eq_coordinates R D F ι φ hφ n ξ q j hrel hξ htame S,
211     standardArtin_eq_coordinates R D F ι hιrange φ hφ n ξ q j hrel hξ htame]
212   split_ifs <;> simp
213 
214 include htame in
215 /-- The finite packet Swan expression and the standard Swan conductor agree. -/
216 theorem packetSwan_eq_standardSwan (S : Finset ℕ) :
217     ((packetSwan R D F n ξ S : ℚ) : ℝ) =
218       swan R D F (actualParameter R D F n ξ) := by
219   rw [packetSwan_eq_zero R D F n ξ htame S,
220     standardSwan_eq_zero R D F n ξ htame]
221   simp
222 
223 /-- Equality of the finite cyclic invariant space with the actual zeroth lower
224 fixed space, packaged as a linear equivalence for Frobenius transport. -/
225 def tameInvariantsEquivFixedZero :
226     (tameRestriction (actualParameter R D F n ξ) ι).invariants ≃ₗ[ℂ]
227       fixed R D F (actualParameter R D F n ξ) 0 :=
228   LinearEquiv.ofEq _ _
229     (fixed_zero_eq_tame_invariants R D F ι hιrange n ξ).symm
230 
231 /-- Frobenius on the actual inertia-fixed space, obtained by transporting the
232 literal induced Frobenius operator through the proved fixed-space equality. -/
233 def actualFixedFrobenius :
234     Module.End ℂ (fixed R D F (actualParameter R D F n ξ) 0) :=
235   (tameInvariantsEquivFixedZero R D F ι hιrange n ξ).conj
236     (InvariantPolynomial.fixedFrobenius
237       (tameRestriction (actualParameter R D F n ξ) ι)
238       (actionEquiv (actualParameter R D F n ξ) φ) q
239       (geometric_relation (actualParameter R D F n ξ) ι φ q hrel)).toLinearMap
240 
241 /-- The standard local polynomial on the actual inertia-fixed space. -/
242 def actualLocalPolynomial : ℂ[X] :=
243   InvariantPolynomial.operatorPolynomial
244     (actualFixedFrobenius R D F ι hιrange φ n ξ q hrel)
245 
246 /-- The finite packet local polynomial is the polynomial of Frobenius on the
247 actual zeroth lower fixed space. -/
248 theorem packetLocalPolynomial_eq_actualLocalPolynomial :
249     InvariantPolynomial.localPolynomial
250       (tameRestriction (actualParameter R D F n ξ) ι)
251       (actionEquiv (actualParameter R D F n ξ) φ) q
252       (geometric_relation (actualParameter R D F n ξ) ι φ q hrel) =
253       actualLocalPolynomial R D F ι hιrange φ n ξ q hrel := by
254   change InvariantPolynomial.operatorPolynomial
255       (InvariantPolynomial.fixedFrobenius
256         (tameRestriction (actualParameter R D F n ξ) ι)
257         (actionEquiv (actualParameter R D F n ξ) φ) q
258         (geometric_relation (actualParameter R D F n ξ) ι φ q hrel)).toLinearMap =
259     InvariantPolynomial.operatorPolynomial
260       ((tameInvariantsEquivFixedZero R D F ι hιrange n ξ).conj
261         (InvariantPolynomial.fixedFrobenius
262           (tameRestriction (actualParameter R D F n ξ) ι)
263           (actionEquiv (actualParameter R D F n ξ) φ) q
264           (geometric_relation (actualParameter R D F n ξ) ι φ q hrel)).toLinearMap)
265   exact (InvariantPolynomial.operatorPolynomial_conj
266     (tameInvariantsEquivFixedZero R D F ι hιrange n ξ)
267     (InvariantPolynomial.fixedFrobenius
268       (tameRestriction (actualParameter R D F n ξ) ι)
269       (actionEquiv (actualParameter R D F n ξ) φ) q
270       (geometric_relation (actualParameter R D F n ξ) ι φ q hrel)).toLinearMap).symm
271 
272 include hφ hrel hξ in
273 /-- Triviality on the actual inertia kernel is equivalent to the zero inertia
274 label of the induced tame packet. -/
275 theorem inertia_le_kernel_iff_label_zero :
276     (actualDegree R D F).ker ≤ (actualParameter R D F n ξ).ker ↔ j = 0 := by
277   constructor
278   · intro hI
279     have hkerTop : Representation.invariants
280         ((actualParameter R D F n ξ).comp (actualDegree R D F).ker.subtype) = ⊤ :=
281       (NormalInertia.fixed_top_iff_le_kernel
282         (actualParameter R D F n ξ) (actualDegree R D F).ker).2 hI
283     have hfiniteTop :
284         (tameRestriction (actualParameter R D F n ξ) ι).invariants = ⊤ :=
285       (invariants_eq_of_range_eq (actualParameter R D F n ξ) ι
286         (actualDegree R D F).ker hιrange).trans hkerTop
287     have htopdim : Module.finrank ℂ
288         (tameRestriction (actualParameter R D F n ξ) ι).invariants =
289         Module.finrank ℂ (DegreeIndSpace (actualDegree R D F) n ξ) :=
290       (LinearEquiv.ofTop _ hfiniteTop).finrank_eq
291     have hdim := InducedTameProfile.invariant_dimension
292       (actualDegree R D F) ι φ hφ n ξ q j hrel hξ
293     rw [htopdim, InducedCycleInvariants.dimension (actualDegree R D F) φ hφ n ξ] at hdim
294     by_contra hj
295     rw [if_neg hj] at hdim
296     exact (NeZero.ne n) hdim.symm
297   · intro hj
298     have hfiniteTop :
299         (tameRestriction (actualParameter R D F n ξ) ι).invariants = ⊤ := by
300       simpa [hj] using InducedTameProfile.inertia_invariants
301         (actualDegree R D F) ι φ hφ n ξ q j hrel hξ
302     have hkerTop : Representation.invariants
303         ((actualParameter R D F n ξ).comp (actualDegree R D F).ker.subtype) = ⊤ := by
304       rw [← invariants_eq_of_range_eq (actualParameter R D F n ξ) ι
305         (actualDegree R D F).ker hιrange]
306       exact hfiniteTop
307     exact (NormalInertia.fixed_top_iff_le_kernel
308       (actualParameter R D F n ξ) (actualDegree R D F).ker).1 hkerTop
309 
310 /-- The actual finite packet record, using the literal lower-group images and
311 lower-numbering weights rather than a supplied abstract filtration. -/
312 def actualObserved {k : Type*} [Field k] [Fintype k]
313     (S : Finset ℕ) (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
314     FiniteTameComparison.Observables M :=
315   FiniteTameComparison.observed (actualDegree R D F) ι φ n ξ q hrel S
316     (fun r => lowerImage R D F (r + 1))
317     (fun r => lowerWeight R D (r + 1)) χ ψ
318 
319 include hφ hrel hξ htame in
320 /-- One source-facing theorem: the actual lower filtration supplies the finite
321 packet coordinates, their local polynomial is Frobenius on the actual inertia
322 fixed space, and the packet conductors equal the standard lower-numbering sums. -/
323 theorem actual_comparison_package {k : Type*} [Field k] [Fintype k]
324     (S : Finset ℕ) (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
325     actualObserved R D F ι φ n ξ q hrel S χ ψ =
326       FiniteTameComparison.fromCoordinates n q j
327         (InducedCycleInvariants.returnScalar (actualDegree R D F) φ hφ n ξ) χ ψ ∧
328     (((actualObserved R D F ι φ n ξ q hrel S χ ψ).finiteSwan : ℚ) : ℝ) =
329       swan R D F (actualParameter R D F n ξ) ∧
330     (((actualObserved R D F ι φ n ξ q hrel S χ ψ).finiteArtin : ℚ) : ℝ) =
331       artin R D F (actualParameter R D F n ξ) ∧
332     (actualObserved R D F ι φ n ξ q hrel S χ ψ).localPolynomial =
333       actualLocalPolynomial R D F ι hιrange φ n ξ q hrel := by
334   have hP : ∀ g ∈ lowerImage R D F 1, ∀ v,
335       actualParameter R D F n ξ g v = v := by
336     intro g hg v
337     obtain ⟨h, rfl⟩ := hg
338     exact LinearMap.congr_fun (htame h) v
339   have hJP : ∀ r ∈ S,
340       lowerImage R D F (r + 1) ≤ lowerImage R D F 1 := by
341     intro r hr g hg
342     obtain ⟨h, rfl⟩ := hg
343     let h1 : lower R D 1 :=
344       RamificationPolyphase.lowerInclusion (R := R) (D := D)
345         (Nat.le_add_left 1 r) h
346     refine ⟨h1, ?_⟩
347     exact (RamificationPolyphase.lift_lowerInclusion (R := R) (D := D)
348       (F := F) (Nat.le_add_left 1 r) h).symm
349   refine ⟨?_, ?_, ?_, ?_⟩
350   · exact FiniteTameComparison.observations_eq_coordinates
351       (actualDegree R D F) ι φ hφ n ξ q j hrel hξ
352       (lowerImage R D F 1) hP S
353       (fun r => lowerImage R D F (r + 1))
354       (fun r => lowerWeight R D (r + 1)) hJP χ ψ
355   · change ((packetSwan R D F n ξ S : ℚ) : ℝ) = _
356     exact packetSwan_eq_standardSwan R D F n ξ htame S
357   · change ((packetArtin R D F ι n ξ S : ℚ) : ℝ) = _
358     exact packetArtin_eq_standardArtin R D F ι hιrange φ hφ n ξ q j hrel hξ htame S
359   · exact packetLocalPolynomial_eq_actualLocalPolynomial
360       R D F ι hιrange φ n ξ q hrel
361 
362 end ActualTameParameter
363 
364 section DescentToCurrentLocalField
365 
366 variable (R D : Type*) [CommRing R] [IsLocalRing R]
367   [Group D] [Fintype D] [MulSemiringAction D R]
368 variable (F : RingAut (IsLocalRing.ResidueField R))
369 variable {M n : ℕ} [NeZero M] [NeZero n]
370 variable (ι : Multiplicative (ZMod M) →*
371   Pullback (residue R D) F)
372 variable (hιrange : ι.range = (degree (residue R D) F).ker)
373 variable (φ : Pullback (residue R D) F)
374 variable (hφ : degree (residue R D) F φ = Multiplicative.ofAdd (1 : ℤ))
375 variable (ξ : TameDegree.degreeSubgroup (degree (residue R D) F) n →* ℂˣ)
376 variable (q : (ZMod M)ˣ) (j : ZMod M)
377 variable (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
378   ι (Multiplicative.ofAdd (q : ZMod M)))
379 variable (hξ : ∀ a : ZMod M,
380   (ξ (InducedTameProfile.inertiaInDegree (degree (residue R D) F) ι n
381     (Multiplicative.ofAdd a)) : ℂ) = ZMod.stdAddChar (j * a))
382 variable [FiniteDimensional ℂ
383   (DegreeIndSpace (degree (residue R D) F) n ξ)]
384 
385 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
386   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
387 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
388   [FiniteDimensional 𝓀[K] s]
389 variable (hF : F ∈ (residue R D).range)
390 
391 /-- The zero-label actual monomial parameter descends uniquely to the current
392 integer-degree unramified Weil model. -/
393 def descendedParameter (hj : j = 0) :
394     Representation ℂ (FiniteUnramifiedWeil.UnramifiedWeil K s)
395       (DegreeIndSpace (degree (residue R D) F) n ξ) :=
396   RamifiedUnramifiedQuotient.descendRepresentation
397     (residue R D) F K s hF
398     (degreeInduced (degree (residue R D) F) n ξ)
399     ((inertia_le_kernel_iff_label_zero R D F ι hιrange φ hφ n ξ q j hrel hξ).2 hj)
400 
401 /-- Pulling the descended parameter back recovers the constructed ramified
402 parameter literally. -/
403 theorem descendedParameter_comp_degreeModelMap (hj : j = 0) :
404     (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj).comp
405       (RamifiedUnramifiedQuotient.degreeModelMap (residue R D) F K s) =
406     degreeInduced (degree (residue R D) F) n ξ :=
407   RamifiedUnramifiedQuotient.descendRepresentation_comp_degreeModelMap
408     (residue R D) F K s hF
409     (degreeInduced (degree (residue R D) F) n ξ)
410     ((inertia_le_kernel_iff_label_zero R D F ι hιrange φ hφ n ξ q j hrel hξ).2 hj)
411 
412 /-- The actual monomial parameter descends to the inertia-free model exactly in
413 the zero inertia-label case. -/
414 theorem exists_unramified_descent_iff :
415     (∃ σ : Representation ℂ (FiniteUnramifiedWeil.UnramifiedWeil K s)
416         (DegreeIndSpace (degree (residue R D) F) n ξ),
417       σ.comp (RamifiedUnramifiedQuotient.degreeModelMap
418         (residue R D) F K s) =
419         degreeInduced (degree (residue R D) F) n ξ) ↔ j = 0 := by
420   constructor
421   · rintro ⟨σ, hσ⟩
422     have hI := RamifiedUnramifiedQuotient.inertia_le_pullbackDegreeRepresentation_ker
423       (residue R D) F K s σ
424     have hker : (degree (residue R D) F).ker ≤
425         (degreeInduced (degree (residue R D) F) n ξ).ker := by
426       simpa only [RamifiedUnramifiedQuotient.Inertia,
427         RamifiedUnramifiedQuotient.pullbackDegreeRepresentation] using
428         (show RamifiedUnramifiedQuotient.Inertia (residue R D) F ≤
429           (σ.comp (RamifiedUnramifiedQuotient.degreeModelMap
430             (residue R D) F K s)).ker from hI)
431     exact (inertia_le_kernel_iff_label_zero R D F ι hιrange φ hφ n ξ q j hrel hξ).1
432       (by simpa [hσ] using hker)
433   · intro hj
434     exact ⟨descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj,
435       descendedParameter_comp_degreeModelMap R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj⟩
436 
437 variable (t : Type*) [Field t] [Algebra s t] [FiniteDimensional s t]
438 
439 /-- Actual unramified field-tower restriction of the descended monomial
440 parameter agrees with the Block 40 degree-dilation polynomial. -/
441 theorem descended_actual_baseChange_polynomial (hj : j = 0) :
442     FiniteUnramifiedWeil.frobeniusPolynomial
443       (UnramifiedFieldTower.LowerField K s) t
444       (UnramifiedFieldTower.restrictRepresentation K s t
445         (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj)) =
446     FiniteUnramifiedWeil.frobeniusPolynomial K s
447       (FiniteUnramifiedWeil.baseChangeRepresentation K s
448         (Module.finrank s t)
449         (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj)) :=
450   ActualUnramifiedBaseChange.frobeniusPolynomial_eq_modelBaseChange K s t
451     (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj)
452 
453 /-- The corresponding Euler factors agree under the actual unramified field
454 tower and the internal monomial degree dilation. -/
455 theorem descended_actual_baseChange_localFactor (hj : j = 0) :
456     FiniteUnramifiedWeil.unramifiedLocalFactor
457       (UnramifiedFieldTower.LowerField K s) t
458       (UnramifiedFieldTower.restrictRepresentation K s t
459         (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj)) =
460     FiniteUnramifiedWeil.unramifiedLocalFactor K s
461       (FiniteUnramifiedWeil.baseChangeRepresentation K s
462         (Module.finrank s t)
463         (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj)) :=
464   ActualUnramifiedBaseChange.localFactor_eq_modelBaseChange K s t
465     (descendedParameter R D F ι hιrange φ hφ n ξ q j hrel hξ K s hF hj)
466 
467 end DescentToCurrentLocalField
468 
469 end PaperXI.ActualMonomialLocalGlobal

Back to source controls