DerivedHeckeAction.lean

1 import PaperXII.PerfectDerivedSupport
2 import PaperXII.HeckeFibers
3 import Mathlib.Algebra.Homology.Linear
4 import Mathlib.Algebra.Homology.ShortComplex.Linear
5 
6 /-!
7 # Hecke operators on actual specialized cohomology
8 
9 The operator starts as multiplication on the original cochain complex. We
10 extend that cochain map, localize it into the actual derived category, and
11 apply the actual cohomology functor. The scalar formula is proved from the
12 tensor relation and the natural comparison with cochain homology.
13 -/
14 
15 noncomputable section
16 
17 open CategoryTheory CategoryTheory.Limits
18 open scoped TensorProduct
19 
20 universe u
21 
22 attribute [local instance] HasDerivedCategory.standard
23 
24 namespace PaperXII.DerivedHeckeAction
25 
26 open ComplexBaseChange PerfectDerivedSupport
27 
28 variable {T E : Type u} [CommRing T] [Field E]
29 
30 /-- The original multiplication endomorphism of the whole cochain complex. -/
31 def cochainOperator (C : CochainComplex (ModuleCat.{u} T) ℤ) (t : T) : C ⟶ C :=
32   t • 𝟙 C
33 
34 /-- Extension of the original module endomorphism satisfies the tensor scalar relation. -/
35 theorem extendScalars_smul_id (y : T →+* E) (M : ModuleCat.{u} T) (t : T) :
36     (ModuleCat.extendScalars y).map (t • 𝟙 M) =
37       y t • 𝟙 ((ModuleCat.extendScalars y).obj M) := by
38   let : Algebra T E := y.toAlgebra
39   apply ModuleCat.hom_ext
40   change HeckeFibers.heckeOperator (H := M) y t = y t • LinearMap.id
41   exact HeckeFibers.heckeOperator_eq_scalar y t
42 
43 /-- The specialized cochain map is proved to be scalar multiplication in every degree. -/
44 theorem baseChange_cochainOperator (C : CochainComplex (ModuleCat.{u} T) ℤ)
45     (y : T →+* E) (t : T) :
46     (complexFunctor y).map (cochainOperator C t) = y t • 𝟙 (baseChange y C) := by
47   apply HomologicalComplex.Hom.ext
48   funext n
49   exact extendScalars_smul_id y (C.X n) t
50 
51 /-- Homology of an actual cochain map preserves scalar multiplication. -/
52 theorem homologyMap_smul {C D : CochainComplex (ModuleCat.{u} E) ℤ}
53     (f : C ⟶ D) (a : E) (n : ℤ) :
54     HomologicalComplex.homologyMap (a • f) n =
55       a • HomologicalComplex.homologyMap f n := by
56   unfold HomologicalComplex.homologyMap
57   change ShortComplex.homologyMap
58     (a • (HomologicalComplex.shortComplexFunctor (ModuleCat E) (.up ℤ) n).map f) = _
59   exact ShortComplex.homologyMap_smul _ _
60 
61 /-- The actual derived cohomology of the specialized complex. -/
62 abbrev specializedCohomology (C : CochainComplex (ModuleCat.{u} T) ℤ)
63     (y : T →+* E) (n : ℤ) : ModuleCat.{u} E :=
64   (DerivedCategory.homologyFunctor (ModuleCat E) n).obj
65     (DerivedCategory.Q.obj (baseChange y C))
66 
67 /-- Apply scalar extension, derived localization, then cohomology to the original operator. -/
68 def cohomologyOperator (C : CochainComplex (ModuleCat.{u} T) ℤ)
69     (y : T →+* E) (n : ℤ) (t : T) :
70     specializedCohomology C y n ⟶ specializedCohomology C y n :=
71   (DerivedCategory.homologyFunctor (ModuleCat E) n).map
72     (DerivedCategory.Q.map ((complexFunctor y).map (cochainOperator C t)))
73 
74 /-- The induced operator on actual derived cohomology is the prescribed scalar. -/
75 theorem cohomologyOperator_eq_scalar (C : CochainComplex (ModuleCat.{u} T) ℤ)
76     (y : T →+* E) (n : ℤ) (t : T) :
77     cohomologyOperator C y n t = y t • 𝟙 (specializedCohomology C y n) := by
78   unfold cohomologyOperator
79   rw [baseChange_cochainOperator]
80   apply (cancel_mono ((DerivedCategory.homologyFunctorFactors (ModuleCat E) n).hom.app
81     (baseChange y C))).mp
82   rw [DerivedCategory.homologyFunctorFactors_hom_naturality, homologyMap_smul,
83     HomologicalComplex.homologyMap_id]
84   ext v
85   exact map_smul ((DerivedCategory.homologyFunctorFactors (ModuleCat E) n).hom.app
86     (baseChange y C)).hom (y t) v |>.symm
87 
88 /-- Every actual specialized cohomology vector has the resulting common eigenvalues. -/
89 theorem cohomologyOperator_apply (C : CochainComplex (ModuleCat.{u} T) ℤ)
90     (y : T →+* E) (n : ℤ) (t : T) (v : specializedCohomology C y n) :
91     cohomologyOperator C y n t v = y t • v := by
92   rw [cohomologyOperator_eq_scalar]
93   rfl
94 
95 /-- The same induced operator for a perfect derived object, using its projective model. -/
96 abbrev perfectCohomologyOperator (P : PerfectComplex T) (y : T →+* E)
97     (n : ℤ) (t : T) :
98     (DerivedCategory.homologyFunctor (ModuleCat E) n).obj (P.baseChange y).object ⟶
99       (DerivedCategory.homologyFunctor (ModuleCat E) n).obj (P.baseChange y).object :=
100   cohomologyOperator P.model.complex y n t
101 
102 /-- The actual operator on a perfect derived fiber is scalar on its cohomology. -/
103 theorem perfectCohomologyOperator_eq_scalar (P : PerfectComplex T) (y : T →+* E)
104     (n : ℤ) (t : T) :
105     perfectCohomologyOperator P y n t = y t •
106       𝟙 ((DerivedCategory.homologyFunctor (ModuleCat E) n).obj (P.baseChange y).object) :=
107   cohomologyOperator_eq_scalar P.model.complex y n t
108 
109 /-- Vector form of the perfect derived specialization formula. -/
110 theorem perfectCohomologyOperator_apply (P : PerfectComplex T) (y : T →+* E)
111     (n : ℤ) (t : T)
112     (v : (DerivedCategory.homologyFunctor (ModuleCat E) n).obj (P.baseChange y).object) :
113     perfectCohomologyOperator P y n t v = y t • v :=
114   cohomologyOperator_apply P.model.complex y n t v
115 
116 end PaperXII.DerivedHeckeAction

Back to source controls