GeneralReconstructionRecovery.lean

1 import PaperX.MonodromyReconstruction
2 import PaperX.LogarithmicRecovery
3 import PaperX.ReconstructionRecovery
4 import PaperX.WeilMorphisms
5 
6 /-! Recover the original group action and monodromy from reconstructed actions
7 for arbitrary nilpotence orders. A supplied common sample must have trivial
8 original action and a nonzero cocycle value. Arithmetic existence of such a
9 sample, and attachment to arbitrary Galois representations, remain separate. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperX.GeneralReconstructionRecovery
13 open PaperX.WeilData PaperX.WeilMorphisms
14 open PaperX.MonodromyReconstruction PaperX.NilpotentExponential
15 open PaperX.LogarithmicRecovery
16 variable {K G : Type*} [Field K] [CharZero K] [Group G] {ν : G →* Kˣ}
17 variable {V W : Type*} [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
18 
19 /-- An actual reconstructed-action intertwiner recovers the monodromy relation
20 from a single supplied nonzero unipotent sample. -/
21 theorem recover_monodromy {D : Datum ν V} {E : Datum ν W}
22     (t : TwistedCocycle ν)
23     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
24     (f : V →ₗ[K] W)
25     (hf : ∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) :
26     E.N ∘ₗ f = f ∘ₗ D.N := by
27   apply (expN_intertwines_iff D.nilpotent E.nilpotent f htu).mp
28   ext x
29   simpa [unipotent, hDu, hEu] using (hf u x).symm
30 
31 /-- Once monodromy is recovered, inverse exponentials recover the original group action. -/
32 theorem recover_group {D : Datum ν V} {E : Datum ν W}
33     (t : TwistedCocycle ν) (f : V →ₗ[K] W)
34     (hN : E.N ∘ₗ f = f ∘ₗ D.N)
35     (hf : ∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x))
36     (g : G) (x : V) : f (D.r g x) = E.r g (f x) :=
37   PaperX.ReconstructionRecovery.recover_group t f hN hf g x
38 
39 /-- The recovered map is equivariant for both the original Weil action and N. -/
40 def recoverHom {D : Datum ν V} {E : Datum ν W}
41     (t : TwistedCocycle ν)
42     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
43     (f : V →ₗ[K] W)
44     (hf : ∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) : Hom D E where
45   map := f
46   group_eq := recover_group t f (recover_monodromy t u hDu hEu htu f hf) hf
47   monodromy_eq x :=
48     (LinearMap.congr_fun (recover_monodromy t u hDu hEu htu f hf) x).symm
49 
50 /-- Under the explicit common-sample hypotheses, reconstructed-action intertwiners
51 are exactly the maps respecting both components of the original datum. -/
52 theorem reconstruct_intertwiner_iff {D : Datum ν V} {E : Datum ν W}
53     (t : TwistedCocycle ν)
54     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
55     (f : V →ₗ[K] W) :
56     (∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) ↔
57       (∀ g x, f (D.r g x) = E.r g (f x)) ∧ E.N ∘ₗ f = f ∘ₗ D.N := by
58   constructor
59   · intro hf
60     have hn := recover_monodromy t u hDu hEu htu f hf
61     exact ⟨recover_group t f hn hf, hn⟩
62   · rintro ⟨hr, hn⟩ g x
63     have hc := expN_intertwines D.nilpotent E.nilpotent f hn (t.value g)
64     change f (expN D.N (t.value g) (D.r g x)) =
65       expN E.N (t.value g) (E.r g (f x))
66     calc
67       _ = expN E.N (t.value g) (f (D.r g x)) := (LinearMap.congr_fun hc _).symm
68       _ = _ := congrArg (expN E.N (t.value g)) (hr g x)
69 
70 /-- With the sample hypotheses fixed, equal reconstructed representations
71 recover equal original actions and equal monodromy operators. -/
72 theorem datum_eq_of_reconstruct_eq {D E : Datum ν V}
73     (t : TwistedCocycle ν)
74     (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1) (htu : t.value u ≠ 0)
75     (hρ : reconstruct D t = reconstruct E t) : D = E := by
76   have hf : ∀ g x, (LinearMap.id : V →ₗ[K] V) (reconstruct D t g x) =
77       reconstruct E t g ((LinearMap.id : V →ₗ[K] V) x) := by
78     intro g x
79     simp only [LinearMap.id_apply, hρ]
80   have h := (reconstruct_intertwiner_iff t u hDu hEu htu LinearMap.id).mp hf
81   apply datum_ext
82   · ext g x
83     exact h.1 g x
84   · simpa only [LinearMap.id_comp, LinearMap.comp_id] using h.2.symm
85 
86 
87 /-- A reconstructed-action projector automatically respects the original
88 monodromy and group action under the same sample hypotheses. -/
89 theorem projector_commutes_original {D : Datum ν V}
90     (t : TwistedCocycle ν) (u : G) (hDu : D.r u = 1) (htu : t.value u ≠ 0)
91     (P : Module.End K V)
92     (hP : ∀ g, P * reconstruct D t g = reconstruct D t g * P) :
93     (∀ g, P * D.r g = D.r g * P) ∧ D.N * P = P * D.N := by
94   have hf : ∀ g x, P (reconstruct D t g x) = reconstruct D t g (P x) :=
95     fun g x => LinearMap.congr_fun (hP g) x
96   have h := (reconstruct_intertwiner_iff t u hDu hDu htu P).mp hf
97   exact ⟨fun g => LinearMap.ext (h.1 g), h.2⟩
98 
99 /-- A reconstructed equivalence recovers the actual local invariant spaces,
100 without any uniform bound on the two nilpotence orders. -/
101 def recoveredFixedEquiv {D : Datum ν V} {E : Datum ν W}
102     (t : TwistedCocycle ν) (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1)
103     (htu : t.value u ≠ 0) (e : V ≃ₗ[K] W)
104     (he : ∀ g x, e (reconstruct D t g x) = reconstruct E t g (e x))
105     (H : Subgroup G) : fixedKernel D H ≃ₗ[K] fixedKernel E H :=
106   let h := (reconstruct_intertwiner_iff t u hDu hEu htu e.toLinearMap).mp he
107   fixedEquiv e h.1 (fun x => (LinearMap.congr_fun h.2 x).symm) H
108 
109 theorem recovered_localCharpoly [FiniteDimensional K V] [FiniteDimensional K W]
110     {D : Datum ν V} {E : Datum ν W}
111     (t : TwistedCocycle ν) (u : G) (hDu : D.r u = 1) (hEu : E.r u = 1)
112     (htu : t.value u ≠ 0) (e : V ≃ₗ[K] W)
113     (he : ∀ g x, e (reconstruct D t g x) = reconstruct E t g (e x))
114     (H : Subgroup G) [H.Normal] (φ : G) :
115     localCharpoly D H φ = localCharpoly E H φ := by
116   have h := (reconstruct_intertwiner_iff t u hDu hEu htu e.toLinearMap).mp he
117   exact localCharpoly_equiv e h.1 (fun x => (LinearMap.congr_fun h.2 x).symm) H φ
118 
119 end PaperX.GeneralReconstructionRecovery

Back to source controls