WeilEuler.lean

1 import PaperX.WeilCopies
2 import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
3 
4 /-! The local Euler denominator is identified with det(1-XF) on the actual
5 inertia-fixed monodromy kernel. No analytic L-function is constructed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.WeilEuler
9 open scoped BigOperators Matrix
10 open Polynomial PaperX.WeilData PaperX.WeilCopies
11 variable {K G : Type*} [Field K] [Group G] {ν : G →* Kˣ}
12 variable {V : Type*} [AddCommGroup V] [Module K V] [FiniteDimensional K V]
13 
14 def eulerPolynomial (D : Datum ν V) (H : Subgroup G) [H.Normal] (φ : G) : Polynomial K :=
15   (localCharpoly D H φ).reverse
16 
17 theorem euler_eq_determinant (D : Datum ν V) (H : Subgroup G) [H.Normal] (φ : G)
18     {J : Type*} [Fintype J] [DecidableEq J] (b : Module.Basis J K (fixedKernel D H)) :
19     eulerPolynomial D H φ =
20       Matrix.det (1 - (X : Polynomial K) • (LinearMap.toMatrix b b (fixedRep D H φ)).map C) := by
21   unfold eulerPolynomial localCharpoly
22   rw [← LinearMap.charpoly_toMatrix _ b, Matrix.reverse_charpoly]
23   rfl
24 
25 theorem euler_constant (D : Datum ν V) (H : Subgroup G) [H.Normal] (φ : G) :
26     (eulerPolynomial D H φ).coeff 0 = 1 := by
27   rw [eulerPolynomial, Polynomial.coeff_zero_reverse]
28   exact (LinearMap.charpoly_monic _).leadingCoeff
29 
30 theorem euler_lift_independent (D : Datum ν V) (H : Subgroup G) [H.Normal]
31     (φ : G) (h : H) : eulerPolynomial D H (φ * h) = eulerPolynomial D H φ := by
32   unfold eulerPolynomial
33   rw [localCharpoly_lift_independent]
34 
35 /-- Over a field, reversal is multiplicative, including zero polynomials. -/
36 def reverseHom : Polynomial K →* Polynomial K where
37   toFun := Polynomial.reverse
38   map_one' := by simpa using (Polynomial.reverse_C (1 : K))
39   map_mul' := Polynomial.reverse_mul_of_domain
40 
41 variable {I : Type*} [Fintype I] {W : I → Type*}
42 variable [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
43 variable [∀ i, FiniteDimensional K (W i)]
44 
45 theorem euler_product (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal]
46     (m : I → ℕ) (φ : G) :
47     eulerPolynomial (copiesDatum D m) H φ = ∏ i, eulerPolynomial (D i) H φ ^ m i := by
48   unfold eulerPolynomial
49   rw [local_charpoly_product]
50   change reverseHom (∏ i, localCharpoly (D i) H φ ^ m i) = _
51   simp only [map_prod, map_pow]
52   rfl
53 
54 theorem common_euler_polynomial {E : Type*} [CommRing E] (σ : E →+* K)
55     (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal] (m : I → ℕ) (φ : G)
56     (P : I → Polynomial E) (hP : ∀ i, eulerPolynomial (D i) H φ = (P i).map σ) :
57     eulerPolynomial (copiesDatum D m) H φ = (∏ i, P i ^ m i).map σ := by
58   rw [euler_product]
59   simp [hP, Polynomial.map_prod]
60 
61 end PaperX.WeilEuler

Back to source controls