ReconstructionRecovery.lean

1 import PaperX.MonodromyReconstruction
2 import PaperX.UnipotentLogarithm
3 import PaperX.WeilMorphisms
4 
5 /-! Recover both pieces of the original datum from reconstructed actions on
6 cubic nilpotence classes. A supplied group element must have trivial original
7 finite action in both data and nonzero cocycle parameter. This theorem does
8 not assert that such an arithmetic sample exists. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.ReconstructionRecovery
12 open PaperX.WeilData PaperX.WeilMorphisms
13 open PaperX.MonodromyReconstruction PaperX.NilpotentExponential
14 open PaperX.UnipotentLogarithm
15 variable {K G : Type*} [Field K] [CharZero K] [Group G] {ν : G →* Kˣ}
16 variable {V W : Type*} [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
17 
18 /-- An actual reconstructed-action intertwiner recovers the monodromy relation
19 from a single supplied nonzero unipotent sample. -/
20 theorem recover_monodromy {D : Datum ν V} {E : Datum ν W}
21     (t : TwistedCocycle ν) (hD : D.N ^ 3 = 0) (hE : E.N ^ 3 = 0)
22     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
23     (f : V →ₗ[K] W)
24     (hf : ∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) :
25     E.N ∘ₗ f = f ∘ₗ D.N := by
26   apply (expN_intertwines_iff hD hE f htu).mp
27   ext x
28   simpa [unipotent, hDu, hEu] using (hf u x).symm
29 
30 /-- Once monodromy is recovered, inverse exponentials recover the original group action. -/
31 theorem recover_group {D : Datum ν V} {E : Datum ν W}
32     (t : TwistedCocycle ν) (f : V →ₗ[K] W)
33     (hN : E.N ∘ₗ f = f ∘ₗ D.N)
34     (hf : ∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x))
35     (g : G) (x : V) : f (D.r g x) = E.r g (f x) := by
36   apply (expEquiv E.nilpotent (t.value g)).injective
37   have hc := expN_intertwines D.nilpotent E.nilpotent f hN (t.value g)
38   change expN E.N (t.value g) (f (D.r g x)) = expN E.N (t.value g) (E.r g (f x))
39   calc
40     _ = f (expN D.N (t.value g) (D.r g x)) := LinearMap.congr_fun hc _
41     _ = _ := hf g x
42 
43 /-- The recovered map is equivariant for both the original Weil action and N. -/
44 def recoverHom {D : Datum ν V} {E : Datum ν W}
45     (t : TwistedCocycle ν) (hD : D.N ^ 3 = 0) (hE : E.N ^ 3 = 0)
46     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
47     (f : V →ₗ[K] W)
48     (hf : ∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) : Hom D E where
49   map := f
50   group_eq := recover_group t f (recover_monodromy t hD hE u hDu hEu htu f hf) hf
51   monodromy_eq x :=
52     (LinearMap.congr_fun (recover_monodromy t hD hE u hDu hEu htu f hf) x).symm
53 
54 /-- Under explicit cubic and sample hypotheses, reconstructed-action intertwiners
55 are exactly the maps respecting both components of the original datum. -/
56 theorem reconstruct_intertwiner_iff {D : Datum ν V} {E : Datum ν W}
57     (t : TwistedCocycle ν) (hD : D.N ^ 3 = 0) (hE : E.N ^ 3 = 0)
58     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
59     (f : V →ₗ[K] W) :
60     (∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) ↔
61       (∀ g x, f (D.r g x) = E.r g (f x)) ∧ E.N ∘ₗ f = f ∘ₗ D.N := by
62   constructor
63   · intro hf
64     have hn := recover_monodromy t hD hE u hDu hEu htu f hf
65     exact ⟨recover_group t f hn hf, hn⟩
66   · rintro ⟨hr, hn⟩ g x
67     have hc := expN_intertwines D.nilpotent E.nilpotent f hn (t.value g)
68     change f (expN D.N (t.value g) (D.r g x)) =
69       expN E.N (t.value g) (E.r g (f x))
70     calc
71       _ = expN E.N (t.value g) (f (D.r g x)) := (LinearMap.congr_fun hc _).symm
72       _ = _ := congrArg (expN E.N (t.value g)) (hr g x)
73 
74 /-- With the sample hypotheses fixed, equal reconstructed representations
75 recover equal original actions and equal monodromy operators. -/
76 theorem datum_eq_of_reconstruct_eq {D E : Datum ν V}
77     (t : TwistedCocycle ν) (hD : D.N ^ 3 = 0) (hE : E.N ^ 3 = 0)
78     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
79     (hρ : reconstruct D t = reconstruct E t) : D = E := by
80   have hf : ∀ g x, (LinearMap.id : V →ₗ[K] V) (reconstruct D t g x) =
81       reconstruct E t g ((LinearMap.id : V →ₗ[K] V) x) := by
82     intro g x
83     simp only [LinearMap.id_apply, hρ]
84   have h := (reconstruct_intertwiner_iff t hD hE u hDu hEu htu LinearMap.id).mp hf
85   apply datum_ext
86   · ext g x
87     exact h.1 g x
88   · simpa only [LinearMap.id_comp, LinearMap.comp_id] using h.2.symm
89 
90 end PaperX.ReconstructionRecovery

Back to source controls