ActualMonomialLocalGlobal.import_only.lean

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

Back to source controls