RankOneEulerFactor.lean

1 import PaperXI.UnramifiedConductorZero
2 import Mathlib.LinearAlgebra.Dimension.Free
3 import Mathlib.Algebra.Polynomial.Reverse
4 
5 /-! # Rank-one Euler factors for irreducible unramified representations -/
6 
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperXI.FiniteUnramifiedWeil
11 
12 open ValuativeRel
13 open scoped Classical Polynomial
14 open Polynomial
15 
16 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
17   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
18 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
19   [FiniteDimensional 𝓀[K] s]
20 
21 section Polynomial
22 
23 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
24 
25 /-- Reversal of a monic linear characteristic polynomial in the convention used
26 throughout Paper XI. -/
27 theorem reverse_X_sub_C (c : ℂ) :
28     (X - C c).reverse = 1 - C c * X := by
29   have hX : (X : ℂ[X]).reverse = 1 := by
30     rw [show (X : ℂ[X]) = X * 1 by simp, Polynomial.reverse_X_mul]
31     simpa using (Polynomial.reverse_C (R := ℂ) (1 : ℂ))
32   rw [sub_eq_add_neg, ← Polynomial.C_neg]
33   rw [Polynomial.reverse_add_C, hX]
34   simp [sub_eq_add_neg]
35 
36 /-- In dimension one, the reverse characteristic polynomial of a homothety is
37 `1 - cX`. -/
38 theorem reverse_charpoly_smul_id (h : Module.finrank ℂ V = 1) (c : ℂ) :
39     ((c • LinearMap.id : Module.End ℂ V).charpoly).reverse = 1 - C c * X := by
40   have hchar : (c • LinearMap.id : Module.End ℂ V).charpoly = X - C c := by
41     rw [show (c • LinearMap.id : Module.End ℂ V) =
42       (0 : Module.End ℂ V) - (-c) • 1 by ext x; simp]
43     rw [LinearMap.charpoly_sub_smul]
44     simp [h, sub_eq_add_neg]
45   rw [hchar]
46   exact reverse_X_sub_C c
47 
48 end Polynomial
49 
50 section Irreducible
51 
52 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
53 variable (ρ : Representation ℂ (UnramifiedWeil K s) V)
54 variable [Representation.IsIrreducible ρ]
55 
56 /-- Scalar by which the distinguished geometric-Frobenius lift acts on an
57 irreducible representation. Irreducibility makes the representation space
58 one-dimensional because the unramified Weil model is commutative. -/
59 noncomputable def frobeniusEigenvalue : ℂ :=
60   (LinearEquiv.smul_id_of_finrank_eq_one
61     (irreducible_finrank_eq_one K s ρ)).symm (ρ (geometricLift K s))
62 
63 /-- The geometric-Frobenius operator is exactly scalar multiplication by the
64 chosen eigenvalue. -/
65 theorem geometricFrobenius_action_eq_smul_id :
66     ρ (geometricLift K s) =
67       frobeniusEigenvalue K s ρ • LinearMap.id := by
68   exact ((LinearEquiv.smul_id_of_finrank_eq_one
69     (irreducible_finrank_eq_one K s ρ)).apply_symm_apply
70       (ρ (geometricLift K s))).symm
71 
72 /-- Frobenius acts invertibly, so its scalar eigenvalue is nonzero. -/
73 theorem frobeniusEigenvalue_ne_zero : frobeniusEigenvalue K s ρ ≠ 0 := by
74   have hdim : 0 < Module.finrank ℂ V := by
75     rw [irreducible_finrank_eq_one K s ρ]
76     exact Nat.zero_lt_one
77   obtain ⟨x, hx⟩ :=
78     (Module.finrank_pos_iff_exists_ne_zero (R := ℂ)).mp hdim
79   intro hzero
80   have hF : ρ (geometricLift K s) = 0 := by
81     rw [geometricFrobenius_action_eq_smul_id K s ρ, hzero]
82     simp
83   have hinv : ρ (geometricLift K s) * ρ ((geometricLift K s)⁻¹) = 1 := by
84     rw [← map_mul]
85     simp
86   rw [hF, zero_mul] at hinv
87   have hpoint := congrArg (fun f : Module.End ℂ V => f x) hinv
88   simp at hpoint
89   exact hx hpoint.symm
90 
91 /-- Explicit linear Euler polynomial for an irreducible representation. -/
92 theorem frobeniusPolynomial_eq_linear :
93     frobeniusPolynomial K s ρ =
94       1 - C (frobeniusEigenvalue K s ρ) * X := by
95   rw [frobeniusPolynomial, geometricFrobenius_action_eq_smul_id K s ρ]
96   exact reverse_charpoly_smul_id
97     (irreducible_finrank_eq_one K s ρ) (frobeniusEigenvalue K s ρ)
98 
99 /-- Reciprocal linear Euler factor associated to a nonzero scalar. -/
100 noncomputable def rankOneEulerFactor (α : ℂ) : RatFunc ℂ :=
101   (algebraMap ℂ[X] (RatFunc ℂ) (1 - C α * X))⁻¹
102 
103 /-- The unramified local factor of an irreducible representation is the expected
104 rank-one Euler factor. -/
105 theorem unramifiedLocalFactor_eq_rankOneEulerFactor :
106     unramifiedLocalFactor K s ρ =
107       rankOneEulerFactor (frobeniusEigenvalue K s ρ) := by
108   rw [unramifiedLocalFactor, rankOneEulerFactor,
109     frobeniusPolynomial_eq_linear K s ρ]
110 
111 end Irreducible
112 
113 end PaperXI.FiniteUnramifiedWeil

Back to source controls