WeilSpecialChain.lean

1 import PaperX.WeilEuler
2 import PaperX.SpecialMonodromy
3 
4 /-! The special monodromy chain is extended to an actual action of the whole
5 group using two characters. Ramified scalar inertia kills every fixed vector. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.WeilSpecialChain
9 open Polynomial PaperX.WeilData PaperX.WeilEuler PaperX.SpecialMonodromy
10 variable {K G : Type*} [Field K] [Group G]
11 
12 def chainRep (ν α : G →* Kˣ) (n : ℕ) : Representation K G (Fin n → K) where
13   toFun g := (diagonalF (ν g) (α g) n).toLinearMap
14   map_one' := by apply LinearMap.ext; intro x; funext j; simp [diagonalF]
15   map_mul' g h := by
16     apply LinearMap.ext
17     intro x
18     funext j
19     simp [diagonalF, mul_pow, mul_comm, mul_left_comm, mul_assoc]
20 
21 def chainDatum (ν α : G →* Kˣ) (n : ℕ) : Datum ν (Fin n → K) where
22   r := chainRep ν α n
23   N := shift n
24   nilpotent := ⟨n, shift_nilpotent n⟩
25   relation g := chain_relation (ν g) (α g) n
26 
27 theorem inertia_scalar (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G)
28     (hν : ∀ h : H, ν h = 1) (h : H) (x : Fin n → K) :
29     (chainDatum ν α n).r h x = (α h : K) • x := by
30   funext j
31   simp [chainDatum, chainRep, diagonalF, hν h]
32 
33 theorem unramified_fixed (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G)
34     (hν : ∀ h : H, ν h = 1) (hα : ∀ h : H, α h = 1) :
35     fixedKernel (chainDatum ν α n) H = LinearMap.ker (shift (K := K) n) := by
36   apply fixedKernel_eq_kernel
37   intro h
38   apply LinearMap.ext
39   intro x
40   rw [inertia_scalar ν α n H hν h x, hα h]
41   simp
42 
43 /-- The unramified local space is the earlier kernel, with the same actual F-action. -/
44 def unramifiedKernelEquiv (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G)
45     (hν : ∀ h : H, ν h = 1) (hα : ∀ h : H, α h = 1) :
46     fixedKernel (chainDatum ν α n) H ≃ₗ[K] LinearMap.ker (shift (K := K) n) :=
47   LinearEquiv.ofEq _ _ (unramified_fixed ν α n H hν hα)
48 
49 theorem unramified_charpoly (ν α : G →* Kˣ) (n : ℕ) (hn : 0 < n)
50     (H : Subgroup G) [H.Normal] (hν : ∀ h : H, ν h = 1)
51     (hα : ∀ h : H, α h = 1) (φ : G) :
52     localCharpoly (chainDatum ν α n) H φ = X - C (α φ : K) := by
53   let e := unramifiedKernelEquiv ν α n H hν hα
54   have he : e.conj (fixedRep (chainDatum ν α n) H φ) =
55       (PaperX.MonodromyData.kernelF (specialDatum (ν φ) (α φ) n)).toLinearMap := by
56     apply LinearMap.ext
57     intro x
58     apply Subtype.ext
59     rfl
60   unfold localCharpoly
61   rw [← LinearEquiv.charpoly_conj e, he]
62   exact special_kernel_charpoly (ν φ) (α φ) n hn
63 
64 theorem ramified_fixed (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G)
65     (hν : ∀ h : H, ν h = 1) (hα : ∃ h : H, α h ≠ 1) :
66     fixedKernel (chainDatum ν α n) H = ⊥ := by
67   obtain ⟨h, hh⟩ := hα
68   apply eq_bot_iff.mpr
69   intro x hx
70   change x = 0
71   have hf : (α h : K) • x = x :=
72     (inertia_scalar ν α n H hν h x).symm.trans (hx.2 h)
73   have hz : ((α h : K) - 1) • x = 0 := by rw [sub_smul, one_smul, hf, sub_self]
74   have ha : (α h : K) - 1 ≠ 0 := sub_ne_zero.mpr (by
75     intro he
76     apply hh
77     apply Units.ext
78     exact he)
79   exact (smul_eq_zero.mp hz).resolve_left ha
80 
81 theorem unramified_dimension (ν α : G →* Kˣ) (n : ℕ) (hn : 0 < n)
82     (H : Subgroup G) (hν : ∀ h : H, ν h = 1) (hα : ∀ h : H, α h = 1) :
83     Module.finrank K (fixedKernel (chainDatum ν α n) H) = 1 := by
84   rw [unramified_fixed ν α n H hν hα, (kernelLine (K := K) n hn).finrank_eq]
85   simp
86 
87 theorem ramified_dimension (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G)
88     (hν : ∀ h : H, ν h = 1) (hα : ∃ h : H, α h ≠ 1) :
89     Module.finrank K (fixedKernel (chainDatum ν α n) H) = 0 := by
90   rw [ramified_fixed ν α n H hν hα]
91   simp
92 
93 theorem ramified_charpoly (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G) [H.Normal]
94     (hν : ∀ h : H, ν h = 1) (hα : ∃ h : H, α h ≠ 1) (φ : G) :
95     localCharpoly (chainDatum ν α n) H φ = 1 := by
96   have hd : (localCharpoly (chainDatum ν α n) H φ).natDegree = 0 := by
97     rw [localCharpoly, LinearMap.charpoly_natDegree, ramified_dimension ν α n H hν hα]
98   have hc : (localCharpoly (chainDatum ν α n) H φ).coeff 0 = 1 := by
99     rw [← hd]
100     exact (LinearMap.charpoly_monic _).leadingCoeff
101   rw [Polynomial.eq_C_of_natDegree_eq_zero hd, hc, Polynomial.C_1]
102 
103 
104 theorem reverse_linear (a : K) : (X - C a).reverse = 1 - C a * X := by
105   have h1 : (1 : Polynomial K).reverse = 1 := by
106     simpa using Polynomial.reverse_C (1 : K)
107   have hx : (X : Polynomial K).reverse = 1 := by
108     simpa [h1] using Polynomial.reverse_mul_X (1 : Polynomial K)
109   rw [sub_eq_add_neg, ← map_neg, Polynomial.reverse_add_C]
110   simp [hx, sub_eq_add_neg]
111 
112 theorem unramified_euler (ν α : G →* Kˣ) (n : ℕ) (hn : 0 < n)
113     (H : Subgroup G) [H.Normal] (hν : ∀ h : H, ν h = 1)
114     (hα : ∀ h : H, α h = 1) (φ : G) :
115     eulerPolynomial (chainDatum ν α n) H φ = 1 - C (α φ : K) * X := by
116   rw [eulerPolynomial, unramified_charpoly ν α n hn H hν hα φ, reverse_linear]
117 
118 theorem ramified_euler (ν α : G →* Kˣ) (n : ℕ) (H : Subgroup G) [H.Normal]
119     (hν : ∀ h : H, ν h = 1) (hα : ∃ h : H, α h ≠ 1) (φ : G) :
120     eulerPolynomial (chainDatum ν α n) H φ = 1 := by
121   rw [eulerPolynomial, ramified_charpoly ν α n H hν hα φ]
122   simpa using Polynomial.reverse_C (1 : K)
123 
124 end PaperX.WeilSpecialChain

Back to source controls