UnramifiedBaseChangeFactor.lean

1 import PaperXI.RankOneEulerFactor
2 
3 /-! # Integer-degree base change for the finite unramified Weil model
4 
5 The finite unramified model is canonically equivalent to `Multiplicative ℤ`.
6 Multiplication of the degree by `n` therefore gives the restriction map that
7 models unramified base change of residue degree `n`. This module proves the
8 resulting Frobenius-power and Euler-factor formulas.
9 
10 No actual tower of local fields is constructed here; the theorem is scoped to
11 this integer-degree Weil model.
12 -/
13 
14 set_option autoImplicit false
15 noncomputable section
16 
17 namespace PaperXI.FiniteUnramifiedWeil
18 
19 open ValuativeRel
20 open PaperXI.ResidueWeil
21 open scoped Classical Polynomial
22 open Polynomial
23 
24 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
25   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
26 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
27   [FiniteDimensional 𝓀[K] s]
28 
29 /-- Multiplication by a natural residue degree on the integral degree group. -/
30 def integerDegreeDilation (n : ℕ) : Multiplicative ℤ →* Multiplicative ℤ where
31   toFun z := Multiplicative.ofAdd ((n : ℤ) * Multiplicative.toAdd z)
32   map_one' := by simp
33   map_mul' a b := by
34     apply Multiplicative.toAdd.injective
35     simp [mul_add]
36 
37 /-- Degree dilation on the finite unramified Weil model. -/
38 def degreeDilation (n : ℕ) : UnramifiedWeil K s →* UnramifiedWeil K s :=
39   (degreeEquiv K s).symm.toMonoidHom.comp
40     ((integerDegreeDilation n).comp (degreeEquiv K s).toMonoidHom)
41 
42 @[simp]
43 theorem degreeEquiv_degreeDilation (n : ℕ) (w : UnramifiedWeil K s) :
44     degreeEquiv K s (degreeDilation K s n w) =
45       integerDegreeDilation n (degreeEquiv K s w) := by
46   simp [degreeDilation]
47 
48 @[simp]
49 theorem degree_degreeDilation (n : ℕ) (w : UnramifiedWeil K s) :
50     Multiplicative.toAdd
51       (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
52         (degreeDilation K s n w)) =
53       (n : ℤ) * Multiplicative.toAdd
54         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) := by
55   change Multiplicative.toAdd (degreeEquiv K s (degreeDilation K s n w)) = _
56   rw [degreeEquiv_degreeDilation]
57   rfl
58 
59 /-- Degree dilation sends the distinguished Frobenius lift to its `n`-th power. -/
60 @[simp]
61 theorem degreeDilation_geometricLift (n : ℕ) :
62     degreeDilation K s n (geometricLift K s) = (geometricLift K s) ^ n := by
63   have hdeg : degreeEquiv K s (geometricLift K s) = Multiplicative.ofAdd 1 := by
64     simpa only [degreeEquiv_apply] using degree_geometricLift K s
65   apply (degreeEquiv K s).injective
66   rw [degreeEquiv_degreeDilation, map_pow, hdeg]
67   apply Multiplicative.toAdd.injective
68   simp [integerDegreeDilation]
69 
70 /-- Successive degree dilations multiply their residue degrees. -/
71 theorem degreeDilation_comp (m n : ℕ) :
72     (degreeDilation K s m).comp (degreeDilation K s n) =
73       degreeDilation K s (m * n) := by
74   apply MonoidHom.ext
75   intro w
76   apply (degreeEquiv K s).injective
77   simp [degreeDilation, integerDegreeDilation, mul_assoc]
78 
79 section Representation
80 
81 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
82 
83 /-- Restriction of a representation along degree dilation. -/
84 def baseChangeRepresentation (n : ℕ)
85     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
86     Representation ℂ (UnramifiedWeil K s) V :=
87   ρ.comp (degreeDilation K s n)
88 
89 /-- Geometric Frobenius after degree-`n` base change acts by the `n`-th power
90 of the original Frobenius operator. -/
91 theorem baseChange_geometricFrobenius (n : ℕ)
92     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
93     baseChangeRepresentation K s n ρ (geometricLift K s) =
94       (ρ (geometricLift K s)) ^ n := by
95   change ρ (degreeDilation K s n (geometricLift K s)) = _
96   rw [degreeDilation_geometricLift]
97   exact map_pow ρ (geometricLift K s) n
98 
99 /-- Base changes compose according to multiplication of residue degrees. -/
100 theorem baseChangeRepresentation_comp (m n : ℕ)
101     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
102     baseChangeRepresentation K s m (baseChangeRepresentation K s n ρ) =
103       baseChangeRepresentation K s (n * m) ρ := by
104   ext w
105   simp [baseChangeRepresentation, degreeDilation, integerDegreeDilation,
106     mul_comm, mul_left_comm, mul_assoc]
107 
108 variable [FiniteDimensional ℂ V]
109 variable (ρ : Representation ℂ (UnramifiedWeil K s) V)
110 
111 /-- Frobenius polynomial transforms by replacing Frobenius with its `n`-th
112 power. -/
113 theorem baseChange_frobeniusPolynomial (n : ℕ)
114     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
115     frobeniusPolynomial K s (baseChangeRepresentation K s n ρ) =
116       ((ρ (geometricLift K s)) ^ n).charpoly.reverse := by
117   rw [frobeniusPolynomial, baseChange_geometricFrobenius]
118 
119 /-- The local factor after degree dilation is the reciprocal characteristic
120 polynomial of the Frobenius power. -/
121 theorem baseChange_localFactor (n : ℕ)
122     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
123     unramifiedLocalFactor K s (baseChangeRepresentation K s n ρ) =
124       (algebraMap ℂ[X] (RatFunc ℂ)
125         (((ρ (geometricLift K s)) ^ n).charpoly.reverse))⁻¹ := by
126   rw [unramifiedLocalFactor, baseChange_frobeniusPolynomial]
127 
128 variable [Representation.IsIrreducible ρ]
129 
130 /-- Rank-one base change raises the Frobenius eigenvalue to the residue degree. -/
131 theorem irreducible_baseChange_frobeniusPolynomial (n : ℕ) :
132     frobeniusPolynomial K s (baseChangeRepresentation K s n ρ) =
133       1 - C ((frobeniusEigenvalue K s ρ) ^ n) * X := by
134   rw [baseChange_frobeniusPolynomial]
135   have hpow : (ρ (geometricLift K s)) ^ n =
136       (frobeniusEigenvalue K s ρ) ^ n • LinearMap.id := by
137     rw [geometricFrobenius_action_eq_smul_id K s ρ]
138     induction n with
139     | zero =>
140         ext x
141         simp
142     | succ n ih =>
143         rw [pow_succ, ih]
144         ext x
145         simp [pow_succ, mul_smul, mul_comm]
146   rw [hpow]
147   exact reverse_charpoly_smul_id
148     (irreducible_finrank_eq_one K s ρ) ((frobeniusEigenvalue K s ρ) ^ n)
149 
150 /-- Explicit Euler-factor base-change law in the irreducible rank-one case. -/
151 theorem irreducible_baseChange_localFactor (n : ℕ) :
152     unramifiedLocalFactor K s (baseChangeRepresentation K s n ρ) =
153       rankOneEulerFactor ((frobeniusEigenvalue K s ρ) ^ n) := by
154   rw [unramifiedLocalFactor, rankOneEulerFactor,
155     irreducible_baseChange_frobeniusPolynomial K s ρ]
156 
157 end Representation
158 
159 end PaperXI.FiniteUnramifiedWeil

Back to source controls