MonodromyReconstruction.lean

1 import PaperX.WeilData
2 import PaperX.NilpotentExponential
3 
4 /-! Finite exponential reconstruction with an explicitly supplied twisted cocycle.
5 No arithmetic tame character or monodromy-existence theorem is assumed proved here. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.MonodromyReconstruction
9 open PaperX.WeilData
10 variable {K G : Type*} [Field K] [CharZero K] [Group G]
11 variable {ν : G →* Kˣ}
12 
13 structure TwistedCocycle (ν : G →* Kˣ) where
14   value : G → K
15   mul_value : ∀ g h, value (g * h) = value g + (ν g : K) * value h
16 
17 omit [CharZero K] in
18 @[simp] theorem cocycle_one (t : TwistedCocycle ν) : t.value 1 = 0 := by
19   have h := t.mul_value 1 1
20   simpa using h
21 
22 variable {V : Type*} [AddCommGroup V] [Module K V]
23 
24 def unipotent (D : Datum ν V) (a : K) : Module.End K V :=
25   PaperX.NilpotentExponential.expN D.N a
26 
27 @[simp] theorem unipotent_zero (D : Datum ν V) : unipotent D 0 = 1 := by
28   simp [unipotent]
29 
30 theorem unipotent_add (D : Datum ν V) (a b : K) :
31     unipotent D (a + b) = unipotent D a * unipotent D b := by
32   exact PaperX.NilpotentExponential.expN_add D.nilpotent a b
33 
34 theorem action_unipotent (D : Datum ν V) (g : G) (a : K) :
35     D.r g * unipotent D a = unipotent D ((ν g : K) * a) * D.r g := by
36   have h : (((ν g : K) * a) • D.N).comp (D.r g) =
37       (D.r g).comp (a • D.N) := by
38     ext x
39     simp [D.relation, smul_smul, mul_comm]
40   let : Module ℚ V := Module.compHom V (algebraMap ℚ K)
41   exact (Module.End.commute_exp_left_of_commute
42     (D.nilpotent.smul a) (D.nilpotent.smul ((ν g : K) * a)) h).symm
43 
44 /-- The exponential is on the left, matching the displayed cocycle law. -/
45 def reconstruct (D : Datum ν V) (t : TwistedCocycle ν) : Representation K G V where
46   toFun g := unipotent D (t.value g) * D.r g
47   map_one' := by simp
48   map_mul' g h := by
49     change unipotent D (t.value (g * h)) * D.r (g * h) =
50       (unipotent D (t.value g) * D.r g) * (unipotent D (t.value h) * D.r h)
51     rw [t.mul_value, unipotent_add, map_mul]
52     simp only [mul_assoc]
53     rw [← mul_assoc (unipotent D ((ν g : K) * t.value h)), ← action_unipotent]
54     simp only [mul_assoc]
55 
56 @[simp] theorem reconstruct_apply (D : Datum ν V) (t : TwistedCocycle ν) (g : G) (x : V) :
57     reconstruct D t g x = unipotent D (t.value g) (D.r g x) := rfl
58 
59 theorem reconstruct_inverse (D : Datum ν V) (t : TwistedCocycle ν) (g : G) :
60     reconstruct D t g * reconstruct D t g⁻¹ = 1 := by
61   rw [← map_mul, mul_inv_cancel, map_one]
62 
63 theorem reconstruct_zero_cocycle (D : Datum ν V) (t : TwistedCocycle ν)
64     (ht : ∀ g, t.value g = 0) : reconstruct D t = D.r := by
65   ext g x
66   simp [ht]
67 
68 omit [CharZero K] in
69 theorem datum_ext {D E : Datum ν V} (hr : D.r = E.r) (hN : D.N = E.N) : D = E := by
70   cases D
71   cases E
72   cases hr
73   cases hN
74   rfl
75 
76 /-- With the nilpotent operator supplied, twisting stays inside the same covariance class. -/
77 def twist (D : Datum ν V) (t : TwistedCocycle ν) : Datum ν V where
78   r := reconstruct D t
79   N := D.N
80   nilpotent := D.nilpotent
81   relation g x := by
82     have hc := PaperX.NilpotentExponential.expN_intertwines D.nilpotent D.nilpotent
83       D.N (by rfl) (t.value g)
84     change unipotent D (t.value g) (D.r g (D.N x)) =
85       (ν g : K) • D.N (unipotent D (t.value g) (D.r g x))
86     rw [D.relation, map_smul]
87     exact congrArg (fun z => (ν g : K) • z) (LinearMap.congr_fun hc (D.r g x))
88 
89 omit [CharZero K] in
90 def negCocycle (t : TwistedCocycle ν) : TwistedCocycle ν where
91   value g := -t.value g
92   mul_value g h := by simp [t.mul_value, add_comm]
93 
94 /-- This inverse keeps N supplied; it does not extract N from an arbitrary representation. -/
95 theorem twist_cancel (D : Datum ν V) (t : TwistedCocycle ν) :
96     twist (twist D t) (negCocycle t) = D := by
97   have hr : (twist (twist D t) (negCocycle t)).r = D.r := by
98     ext g x
99     change (unipotent D (-t.value g) * (unipotent D (t.value g) * D.r g)) x = D.r g x
100     rw [← mul_assoc, show unipotent D (-t.value g) * unipotent D (t.value g) = 1 from
101       PaperX.NilpotentExponential.expN_neg_mul D.nilpotent _, one_mul]
102   exact datum_ext hr rfl
103 
104 theorem reconstruct_on_kernel (D : Datum ν V) (t : TwistedCocycle ν)
105     (g : G) {x : V} (hx : D.N x = 0) : reconstruct D t g x = D.r g x :=
106   PaperX.NilpotentExponential.expN_identity_on_kernel D.nilpotent _ (kernel_stable D g hx)
107 
108 /-- The independently defined fixed kernel is unchanged by the twist. -/
109 theorem twist_fixedKernel (D : Datum ν V) (t : TwistedCocycle ν) (H : Subgroup G) :
110     fixedKernel (twist D t) H = fixedKernel D H := by
111   ext x
112   simp only [mem_fixedKernel]
113   constructor
114   · rintro ⟨hN, hH⟩
115     exact ⟨hN, fun h => (reconstruct_on_kernel D t h hN).symm.trans (hH h)⟩
116   · rintro ⟨hN, hH⟩
117     exact ⟨hN, fun h => (reconstruct_on_kernel D t h hN).trans (hH h)⟩
118 
119 end PaperX.MonodromyReconstruction

Back to source controls