ReconstructionLocal.lean

1 import PaperX.MonodromyReconstruction
2 import PaperX.WeilEuler
3 
4 /-! Local fixed kernels and Euler polynomials are preserved by twisting supplied data. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.ReconstructionLocal
8 open PaperX.WeilData PaperX.MonodromyReconstruction PaperX.WeilEuler
9 variable {K G V : Type*} [Field K] [CharZero K] [Group G]
10 variable {ν : G →* Kˣ} [AddCommGroup V] [Module K V]
11 
12 def localEquiv (D : Datum ν V) (t : TwistedCocycle ν) (H : Subgroup G) :
13     fixedKernel (twist D t) H ≃ₗ[K] fixedKernel D H where
14   toFun x := ⟨x.val, by rw [← twist_fixedKernel D t H]; exact x.property⟩
15   invFun x := ⟨x.val, by rw [twist_fixedKernel D t H]; exact x.property⟩
16   left_inv _ := rfl
17   right_inv _ := rfl
18   map_add' _ _ := rfl
19   map_smul' _ _ := rfl
20 
21 theorem local_equivariant (D : Datum ν V) (t : TwistedCocycle ν) (H : Subgroup G)
22     [H.Normal] (g : G) (x : fixedKernel (twist D t) H) :
23     localEquiv D t H (fixedRep (twist D t) H g x) =
24       fixedRep D H g (localEquiv D t H x) := by
25   apply Subtype.ext
26   exact reconstruct_on_kernel D t g x.property.1
27 
28 theorem local_conjugate (D : Datum ν V) (t : TwistedCocycle ν) (H : Subgroup G)
29     [H.Normal] (g : G) :
30     (localEquiv D t H).conj (fixedRep (twist D t) H g) = fixedRep D H g := by
31   ext x
32   exact reconstruct_on_kernel D t g x.property.1
33 
34 variable [FiniteDimensional K V]
35 
36 theorem twist_localCharpoly (D : Datum ν V) (t : TwistedCocycle ν) (H : Subgroup G)
37     [H.Normal] (φ : G) : localCharpoly (twist D t) H φ = localCharpoly D H φ := by
38   unfold localCharpoly
39   rw [← LinearEquiv.charpoly_conj (localEquiv D t H), local_conjugate]
40 
41 theorem twist_euler (D : Datum ν V) (t : TwistedCocycle ν) (H : Subgroup G)
42     [H.Normal] (φ : G) : eulerPolynomial (twist D t) H φ = eulerPolynomial D H φ := by
43   unfold eulerPolynomial
44   rw [twist_localCharpoly]
45 
46 end PaperX.ReconstructionLocal

Back to source controls