UnramifiedLocalFactor.lean

1 import PaperXI.FiniteUnramifiedWeil
2 import Mathlib.FieldTheory.RatFunc.Basic
3 import Mathlib.RepresentationTheory.Invariants
4 import Mathlib.LinearAlgebra.Charpoly.ToMatrix
5 import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
6 
7 /-! # Unramified local factors for the finite Weil model -/
8 
9 set_option autoImplicit false
10 noncomputable section
11 
12 namespace PaperXI.FiniteUnramifiedWeil
13 
14 open ValuativeRel
15 open PaperXI.ResidueWeil
16 open scoped Classical Polynomial
17 open Polynomial
18 
19 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
20   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
21 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
22   [FiniteDimensional 𝓀[K] s]
23 
24 section Representation
25 
26 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
27 
28 abbrev Inertia : Subgroup (UnramifiedWeil K s) :=
29   (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)).ker
30 
31 /-- Every representation is trivial on the actual inertia subgroup because this
32 finite unramified Weil model has trivial inertia. -/
33 theorem inertia_le_kernel (ρ : Representation ℂ (UnramifiedWeil K s) V) :
34     Inertia K s ≤ ρ.ker := by
35   rw [Inertia, inertia_eq_bot K s]
36   exact bot_le
37 
38 /-- The inertia-fixed subspace is the whole representation space. -/
39 theorem inertia_invariants_eq_top (ρ : Representation ℂ (UnramifiedWeil K s) V) :
40     Representation.invariants (ρ.comp (Inertia K s).subtype) = ⊤ :=
41   (PaperXI.NormalInertia.fixed_top_iff_le_kernel ρ (Inertia K s)).2
42     (inertia_le_kernel K s ρ)
43 
44 /-- Frobenius polynomial of a representation of the finite unramified Weil model.
45 It is the same reverse characteristic-polynomial convention used by the existing
46 Paper XI local-factor modules. -/
47 noncomputable def frobeniusPolynomial [FiniteDimensional ℂ V]
48     (ρ : Representation ℂ (UnramifiedWeil K s) V) : ℂ[X] :=
49   (ρ (geometricLift K s)).charpoly.reverse
50 
51 /-- Rational unramified local factor: reciprocal of the full geometric-Frobenius polynomial. -/
52 noncomputable def unramifiedLocalFactor [FiniteDimensional ℂ V]
53     (ρ : Representation ℂ (UnramifiedWeil K s) V) : RatFunc ℂ :=
54   (algebraMap ℂ[X] (RatFunc ℂ) (frobeniusPolynomial K s ρ))⁻¹
55 
56 
57 /-- The canonical linear equivalence from inertia-fixed vectors to the full
58 space, available because inertia is trivial in the finite unramified model. -/
59 noncomputable def inertiaFixedEquiv (ρ : Representation ℂ (UnramifiedWeil K s) V) :
60     Representation.invariants (ρ.comp (Inertia K s).subtype) ≃ₗ[ℂ] V :=
61   LinearEquiv.ofTop _ (inertia_invariants_eq_top K s ρ)
62 
63 /-- Geometric Frobenius restricted to the actual inertia-fixed subspace. -/
64 noncomputable def fixedGeometricFrobenius
65     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
66     Module.End ℂ (Representation.invariants (ρ.comp (Inertia K s).subtype)) :=
67   (inertiaFixedEquiv K s ρ).symm.conj (ρ (geometricLift K s))
68 
69 @[simp]
70 theorem fixedGeometricFrobenius_charpoly [FiniteDimensional ℂ V]
71     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
72     (fixedGeometricFrobenius K s ρ).charpoly =
73       (ρ (geometricLift K s)).charpoly := by
74   exact (inertiaFixedEquiv K s ρ).symm.charpoly_conj _
75 
76 /-- The local polynomial formed on the literal inertia-fixed subspace. -/
77 noncomputable def inertiaFrobeniusPolynomial [FiniteDimensional ℂ V]
78     (ρ : Representation ℂ (UnramifiedWeil K s) V) : ℂ[X] :=
79   (fixedGeometricFrobenius K s ρ).charpoly.reverse
80 
81 /-- Trivial inertia makes the invariant-space and full-space Frobenius
82 polynomials literally equal. -/
83 theorem inertiaFrobeniusPolynomial_eq [FiniteDimensional ℂ V]
84     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
85     inertiaFrobeniusPolynomial K s ρ = frobeniusPolynomial K s ρ := by
86   unfold inertiaFrobeniusPolynomial frobeniusPolynomial
87   rw [fixedGeometricFrobenius_charpoly]
88 
89 /-- Local factor formed from Frobenius on actual inertia invariants. -/
90 noncomputable def inertiaLocalFactor [FiniteDimensional ℂ V]
91     (ρ : Representation ℂ (UnramifiedWeil K s) V) : RatFunc ℂ :=
92   (algebraMap ℂ[X] (RatFunc ℂ) (inertiaFrobeniusPolynomial K s ρ))⁻¹
93 
94 /-- The invariant-space local factor is the full unramified local factor. -/
95 theorem inertiaLocalFactor_eq [FiniteDimensional ℂ V]
96     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
97     inertiaLocalFactor K s ρ = unramifiedLocalFactor K s ρ := by
98   unfold inertiaLocalFactor unramifiedLocalFactor
99   rw [inertiaFrobeniusPolynomial_eq]
100 
101 set_option maxHeartbeats 800000 in
102 /-- Determinant form of the reverse characteristic polynomial. -/
103 theorem frobeniusPolynomial_eq_det [FiniteDimensional ℂ V]
104     (ρ : Representation ℂ (UnramifiedWeil K s) V)
105     {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℂ V) :
106     frobeniusPolynomial K s ρ =
107       Matrix.det (1 - (X : ℂ[X]) •
108         (LinearMap.toMatrix b b (ρ (geometricLift K s))).map Polynomial.C) := by
109   rw [frobeniusPolynomial, ← LinearMap.charpoly_toMatrix (ρ (geometricLift K s)) b,
110     Matrix.reverse_charpoly]
111   rfl
112 
113 /-- The Frobenius polynomial has constant coefficient one. -/
114 theorem frobeniusPolynomial_coeff_zero [FiniteDimensional ℂ V]
115     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
116     (frobeniusPolynomial K s ρ).coeff 0 = 1 := by
117   rw [frobeniusPolynomial, Polynomial.coeff_zero_reverse]
118   exact (ρ (geometricLift K s)).charpoly_monic.leadingCoeff
119 
120 /-- Evaluation at zero is one. -/
121 theorem frobeniusPolynomial_eval_zero [FiniteDimensional ℂ V]
122     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
123     Polynomial.eval 0 (frobeniusPolynomial K s ρ) = 1 := by
124   rw [← Polynomial.coeff_zero_eq_eval_zero, frobeniusPolynomial_coeff_zero]
125 
126 /-- The Frobenius polynomial is nonzero. -/
127 theorem frobeniusPolynomial_ne_zero [FiniteDimensional ℂ V]
128     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
129     frobeniusPolynomial K s ρ ≠ 0 := by
130   intro h
131   have h0 := frobeniusPolynomial_coeff_zero K s ρ
132   rw [h] at h0
133   simp at h0
134 
135 /-- Its image in the rational-function field is nonzero. -/
136 theorem mappedFrobeniusPolynomial_ne_zero [FiniteDimensional ℂ V]
137     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
138     algebraMap ℂ[X] (RatFunc ℂ) (frobeniusPolynomial K s ρ) ≠ 0 :=
139   (map_ne_zero_iff _ (RatFunc.algebraMap_injective ℂ)).2
140     (frobeniusPolynomial_ne_zero K s ρ)
141 
142 /-- The local factor is a genuine reciprocal of the Frobenius polynomial. -/
143 theorem unramifiedLocalFactor_mul_polynomial [FiniteDimensional ℂ V]
144     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
145     unramifiedLocalFactor K s ρ *
146       algebraMap ℂ[X] (RatFunc ℂ) (frobeniusPolynomial K s ρ) = 1 := by
147   rw [unramifiedLocalFactor]
148   exact inv_mul_cancel₀ (mappedFrobeniusPolynomial_ne_zero K s ρ)
149 
150 /-- The reciprocal identity also holds in the opposite order. -/
151 theorem polynomial_mul_unramifiedLocalFactor [FiniteDimensional ℂ V]
152     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
153     algebraMap ℂ[X] (RatFunc ℂ) (frobeniusPolynomial K s ρ) *
154       unramifiedLocalFactor K s ρ = 1 := by
155   rw [unramifiedLocalFactor]
156   exact mul_inv_cancel₀ (mappedFrobeniusPolynomial_ne_zero K s ρ)
157 
158 /-- The unramified local factor is nonzero. -/
159 theorem unramifiedLocalFactor_ne_zero [FiniteDimensional ℂ V]
160     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
161     unramifiedLocalFactor K s ρ ≠ 0 := by
162   rw [unramifiedLocalFactor]
163   exact inv_ne_zero (mappedFrobeniusPolynomial_ne_zero K s ρ)
164 
165 
166 end Representation
167 
168 end PaperXI.FiniteUnramifiedWeil

Back to source controls