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

Back to source controls