ReconstructionSummands.lean

1 import PaperX.MonodromyReconstruction
2 import PaperX.WeilMorphisms
3 
4 /-! Reconstruction commutes with actual finite-copy actions and split maps. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.ReconstructionSummands
8 open PaperX.WeilData PaperX.WeilCopies PaperX.WeilMorphisms
9 open PaperX.MonodromyReconstruction PaperX.CarrierSummands
10 variable {K G : Type*} [Field K] [CharZero K] [Group G] {ν : G →* Kˣ}
11 variable {V W : Type*} [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
12 
13 theorem reconstruct_intertwines {D : Datum ν V} {E : Datum ν W}
14     (f : Hom D E) (t : TwistedCocycle ν) (g : G) (x : V) :
15     f.map (reconstruct D t g x) = reconstruct E t g (f.map x) := by
16   have hc := PaperX.NilpotentExponential.expN_intertwines D.nilpotent E.nilpotent f.map
17     (LinearMap.ext fun x => (f.monodromy_eq x).symm) (t.value g)
18   change f.map (unipotent D (t.value g) (D.r g x)) = _
19   exact (LinearMap.congr_fun hc (D.r g x)).symm.trans
20     (congrArg (unipotent E (t.value g)) (f.group_eq g x))
21 
22 def twistHom {D : Datum ν V} {E : Datum ν W} (f : Hom D E) (t : TwistedCocycle ν) :
23     Hom (twist D t) (twist E t) where
24   map := f.map
25   group_eq := reconstruct_intertwines f t
26   monodromy_eq := f.monodromy_eq
27 
28 variable {I : Type*} [Fintype I] {X : I → Type*}
29 variable [∀ i, AddCommGroup (X i)] [∀ i, Module K (X i)]
30 
31 omit [CharZero K] in
32 def component (m : I → ℕ) (i : I) (k : Fin (m i)) : Copies X m →ₗ[K] X i where
33   toFun x := x i k
34   map_add' _ _ := rfl
35   map_smul' _ _ := rfl
36 
37 theorem unipotent_copies (D : ∀ i, Datum ν (X i)) (m : I → ℕ) (a : K)
38     (x : Copies X m) (i : I) (k : Fin (m i)) :
39     unipotent (copiesDatum D m) a x i k = unipotent (D i) a (x i k) := by
40   have h := PaperX.NilpotentExponential.expN_intertwines
41     (copiesDatum D m).nilpotent (D i).nilpotent (component m i k) (by rfl) a
42   exact (LinearMap.congr_fun h x).symm
43 
44 theorem reconstruct_copies (D : ∀ i, Datum ν (X i)) (m : I → ℕ)
45     (t : TwistedCocycle ν) :
46     reconstruct (copiesDatum D m) t = copiesRep (fun i => reconstruct (D i) t) m := by
47   ext g x i k
48   exact unipotent_copies D m (t.value g) _ i k
49 
50 theorem twist_copies (D : ∀ i, Datum ν (X i)) (m : I → ℕ)
51     (t : TwistedCocycle ν) :
52     twist (copiesDatum D m) t = copiesDatum (fun i => twist (D i) t) m :=
53   datum_ext (reconstruct_copies D m t) rfl
54 
55 theorem reconstructed_inclusion (D : ∀ i, Datum ν (X i)) (t : TwistedCocycle ν)
56     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (g : G) (x : Copies X m) :
57     inclusion (R := K) h (reconstruct (copiesDatum D m) t g x) =
58       reconstruct (copiesDatum D c) t g (inclusion (R := K) h x) :=
59   reconstruct_intertwines (inclusionHom D h) t g x
60 
61 theorem reconstructed_retraction (D : ∀ i, Datum ν (X i)) (t : TwistedCocycle ν)
62     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (g : G) (x : Copies X c) :
63     retraction (R := K) h (reconstruct (copiesDatum D c) t g x) =
64       reconstruct (copiesDatum D m) t g (retraction (R := K) h x) :=
65   reconstruct_intertwines (retractionHom D h) t g x
66 
67 theorem reconstructed_projector (D : ∀ i, Datum ν (X i)) (t : TwistedCocycle ν)
68     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (g : G) :
69     (projector (R := K) (V := X) h).comp (reconstruct (copiesDatum D c) t g) =
70       (reconstruct (copiesDatum D c) t g).comp (projector h) := by
71   rw [reconstruct_copies]
72   exact projector_equivariant (fun i => reconstruct (D i) t) h g
73 
74 end PaperX.ReconstructionSummands

Back to source controls