ActualUnramifiedBaseChange.lean

1 import PaperXI.UnramifiedFieldTower
2 
3 /-! # Actual unramified base change through the recursive local-field tower
4 
5 Block 40 proved Frobenius-power and Euler-factor formulas for an internal degree
6 dilation of the integer-degree unramified Weil model. Block 41 constructs an
7 actual recursive local-field tower and its restriction map. This module proves
8 that the two constructions give the same Frobenius polynomials and local
9 factors, and records conductor zero on both sides of the actual tower.
10 
11 This remains scoped to the bounded unramified Weil models, not absolute Weil
12 groups or automorphic base change.
13 -/
14 
15 set_option autoImplicit false
16 noncomputable section
17 
18 namespace PaperXI.ActualUnramifiedBaseChange
19 
20 open PaperXI.UnramifiedFieldTower
21 open PaperXI.FiniteUnramifiedWeil
22 open ValuativeRel
23 open scoped Classical Polynomial
24 open Polynomial
25 
26 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
27   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
28 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
29   [FiniteDimensional 𝓀[K] s]
30 variable (t : Type*) [Field t] [Algebra s t] [FiniteDimensional s t]
31 
32 noncomputable local instance : Algebra 𝓀[LowerField K s] t :=
33   residueTowerAlgebra K s t
34 
35 noncomputable local instance : FiniteDimensional 𝓀[LowerField K s] t :=
36   residueTowerFinite K s t
37 
38 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
39 variable (ρ : Representation ℂ (UnramifiedWeil K s) V)
40 
41 /-- Actual tower restriction and Block 40's internal degree dilation have the
42 same Frobenius polynomial. -/
43 theorem frobeniusPolynomial_eq_modelBaseChange :
44     frobeniusPolynomial (LowerField K s) t (restrictRepresentation K s t ρ) =
45       frobeniusPolynomial K s
46         (baseChangeRepresentation K s (Module.finrank s t) ρ) := by
47   rw [restriction_frobeniusPolynomial,
48     baseChange_frobeniusPolynomial, map_pow]
49 
50 /-- Actual tower restriction and the internal degree-dilation model have the
51 same rational unramified local factor. -/
52 theorem localFactor_eq_modelBaseChange :
53     unramifiedLocalFactor (LowerField K s) t
54         (restrictRepresentation K s t ρ) =
55       unramifiedLocalFactor K s
56         (baseChangeRepresentation K s (Module.finrank s t) ρ) := by
57   unfold unramifiedLocalFactor
58   rw [frobeniusPolynomial_eq_modelBaseChange K s t ρ]
59 
60 /-- Inertia codimension remains zero after restriction through the actual
61 unramified tower. -/
62 theorem restricted_inertiaCodimension_eq_zero :
63     inertiaCodimension (LowerField K s) t
64       (restrictRepresentation K s t ρ) = 0 :=
65   inertiaCodimension_eq_zero (LowerField K s) t
66     (restrictRepresentation K s t ρ)
67 
68 omit [FiniteDimensional ℂ V] in
69 /-- Swan conductor remains zero after restriction through the actual
70 unramified tower. -/
71 theorem restricted_swanConductorExponent_eq_zero :
72     swanConductorExponent (LowerField K s) t
73       (restrictRepresentation K s t ρ) = 0 :=
74   swanConductorExponent_eq_zero (LowerField K s) t
75     (restrictRepresentation K s t ρ)
76 
77 /-- Artin conductor remains zero after restriction through the actual
78 unramified tower. -/
79 theorem restricted_artinConductorExponent_eq_zero :
80     artinConductorExponent (LowerField K s) t
81       (restrictRepresentation K s t ρ) = 0 :=
82   artinConductorExponent_eq_zero (LowerField K s) t
83     (restrictRepresentation K s t ρ)
84 
85 /-- The model Artin exponent is invariant under actual unramified tower
86 restriction; both sides vanish for the bounded unramified Weil models. -/
87 theorem artinConductorExponent_restriction :
88     artinConductorExponent (LowerField K s) t
89         (restrictRepresentation K s t ρ) =
90       artinConductorExponent K s ρ := by
91   rw [restricted_artinConductorExponent_eq_zero K s t ρ,
92     artinConductorExponent_eq_zero K s ρ]
93 
94 variable [Representation.IsIrreducible ρ]
95 
96 /-- For an irreducible lower representation, actual field-tower restriction
97 raises the Frobenius eigenvalue to the relative residue degree. -/
98 theorem irreducible_restriction_frobeniusPolynomial :
99     frobeniusPolynomial (LowerField K s) t
100         (restrictRepresentation K s t ρ) =
101       1 - C ((frobeniusEigenvalue K s ρ) ^ Module.finrank s t) * X := by
102   rw [frobeniusPolynomial_eq_modelBaseChange K s t ρ]
103   exact irreducible_baseChange_frobeniusPolynomial K s ρ
104     (Module.finrank s t)
105 
106 /-- Explicit rank-one Euler factor under the actual unramified field tower. -/
107 theorem irreducible_restriction_localFactor :
108     unramifiedLocalFactor (LowerField K s) t
109         (restrictRepresentation K s t ρ) =
110       rankOneEulerFactor
111         ((frobeniusEigenvalue K s ρ) ^ Module.finrank s t) := by
112   rw [localFactor_eq_modelBaseChange K s t ρ]
113   exact irreducible_baseChange_localFactor K s ρ (Module.finrank s t)
114 
115 end PaperXI.ActualUnramifiedBaseChange

Back to source controls