WeilData.lean

1 import PaperX.MonodromyKernels
2 import Mathlib.RepresentationTheory.Invariants
3 
4 /-! Group actions with monodromy, an explicit norm character, and actual
5 inertia-fixed kernels. Arithmetic identification of G and H is separate. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.WeilData
9 variable {K G : Type*} [Field K] [Group G]
10 variable (ν : G →* Kˣ)
11 
12 structure Datum (V : Type*) [AddCommGroup V] [Module K V] where
13   r : Representation K G V
14   N : Module.End K V
15   nilpotent : IsNilpotent N
16   relation : ∀ g x, r g (N x) = (ν g : K) • N (r g x)
17 
18 variable {ν} {V : Type*} [AddCommGroup V] [Module K V]
19 
20 def actionEquiv (ρ : Representation K G V) (g : G) : V ≃ₗ[K] V where
21   toFun := ρ g
22   invFun := ρ g⁻¹
23   left_inv x := by simp [← Module.End.mul_apply, ← map_mul]
24   right_inv x := by simp [← Module.End.mul_apply, ← map_mul]
25   map_add' := (ρ g).map_add
26   map_smul' := (ρ g).map_smul
27 
28 def toMonodromy (D : Datum ν V) (g : G) : PaperX.MonodromyData.Datum (ν g) V where
29   F := actionEquiv D.r g
30   N := D.N
31   nilpotent := D.nilpotent
32   relation := D.relation g
33 
34 def inertiaFixed (H : Subgroup G) (ρ : Representation K G V) : Submodule K V :=
35   Representation.invariants (ρ.comp H.subtype)
36 
37 def fixedKernel (D : Datum ν V) (H : Subgroup G) : Submodule K V :=
38   LinearMap.ker D.N ⊓ inertiaFixed H D.r
39 
40 @[simp] theorem mem_fixedKernel (D : Datum ν V) (H : Subgroup G) (x : V) :
41     x ∈ fixedKernel D H ↔ D.N x = 0 ∧ ∀ h : H, D.r h x = x := Iff.rfl
42 
43 theorem inertia_N_commutes (D : Datum ν V) (H : Subgroup G)
44     (hν : ∀ h : H, ν h = 1) (h : H) (x : V) : D.r h (D.N x) = D.N (D.r h x) := by
45   simpa [hν h] using D.relation h x
46 
47 theorem kernel_stable (D : Datum ν V) (g : G) {x : V} (hx : D.N x = 0) :
48     D.N (D.r g x) = 0 := by
49   have h := D.relation g x
50   rw [hx, map_zero] at h
51   exact (smul_eq_zero.mp h.symm).resolve_left (Units.ne_zero (ν g))
52 
53 theorem inertia_stable (ρ : Representation K G V) (H : Subgroup G) [H.Normal]
54     (g : G) {x : V} (hx : x ∈ inertiaFixed H ρ) : ρ g x ∈ inertiaFixed H ρ := by
55   intro h
56   have hh : g⁻¹ * (h : G) * g ∈ H := by
57     simpa using (inferInstance : H.Normal).conj_mem (h : G) h.property g⁻¹
58   have he := hx (⟨g⁻¹ * (h : G) * g, hh⟩ : H)
59   calc
60     ρ h (ρ g x) = ρ g (ρ (g⁻¹ * (h : G) * g) x) := by
61       simp [← Module.End.mul_apply, ← map_mul, mul_assoc]
62     _ = ρ g x := congrArg (ρ g) he
63 
64 theorem fixedKernel_stable (D : Datum ν V) (H : Subgroup G) [H.Normal]
65     (g : G) {x : V} (hx : x ∈ fixedKernel D H) : D.r g x ∈ fixedKernel D H :=
66   ⟨kernel_stable D g hx.1, inertia_stable D.r H g hx.2⟩
67 
68 /-- The restriction is an actual representation on the independently defined subspace. -/
69 def fixedRep (D : Datum ν V) (H : Subgroup G) [H.Normal] :
70     Representation K G (fixedKernel D H) where
71   toFun g :=
72     { toFun := fun x => ⟨D.r g x.val, fixedKernel_stable D H g x.property⟩
73       map_add' := by intros; apply Subtype.ext; simp
74       map_smul' := by intros; apply Subtype.ext; simp }
75   map_one' := by ext x; simp
76   map_mul' g h := by ext x; simp
77 
78 @[simp] theorem fixedRep_val (D : Datum ν V) (H : Subgroup G) [H.Normal]
79     (g : G) (x : fixedKernel D H) : (fixedRep D H g x).val = D.r g x.val := rfl
80 
81 def fixedF (D : Datum ν V) (H : Subgroup G) [H.Normal] (φ : G) :
82     fixedKernel D H ≃ₗ[K] fixedKernel D H := actionEquiv (fixedRep D H) φ
83 
84 def localCharpoly [FiniteDimensional K V] (D : Datum ν V) (H : Subgroup G)
85     [H.Normal] (φ : G) : Polynomial K := (fixedRep D H φ).charpoly
86 
87 /-- Changing a Frobenius lift by an inertia element leaves its restricted action equal. -/
88 theorem lift_independent (D : Datum ν V) (H : Subgroup G) [H.Normal]
89     (φ : G) (h : H) : fixedRep D H (φ * h) = fixedRep D H φ := by
90   ext x
91   change D.r (φ * h) x.val = D.r φ x.val
92   rw [map_mul, Module.End.mul_apply]
93   exact congrArg (D.r φ) (x.property.2 h)
94 
95 theorem localCharpoly_lift_independent [FiniteDimensional K V]
96     (D : Datum ν V) (H : Subgroup G) [H.Normal] (φ : G) (h : H) :
97     localCharpoly D H (φ * h) = localCharpoly D H φ := by
98   unfold localCharpoly
99   rw [lift_independent]
100 
101 /-- Trivial inertia recovers the earlier monodromy kernel exactly. -/
102 theorem fixedKernel_eq_kernel (D : Datum ν V) (H : Subgroup G)
103     (hr : ∀ h : H, D.r h = 1) : fixedKernel D H = LinearMap.ker D.N := by
104   ext x
105   simp [mem_fixedKernel, hr]
106 
107 end PaperX.WeilData

Back to source controls