HeckeCarriers.lean

1 import PaperXII.DerivedHeckeAction
2 import PaperXII.PerfectCohomology
3 import PaperXII.BaseChangeSupport
4 
5 /-!
6 # Ordinary and derived Hecke carriers
7 
8 The two carriers are an actual finite module and an actual perfect derived
9 object. Their fibers and operators are the tensor module and the specialized
10 derived cohomology, with operators induced by the original multiplication.
11 Support comparisons are literal inclusions of subsets of prime spectra.
12 -/
13 
14 noncomputable section
15 
16 open CategoryTheory CategoryTheory.Limits
17 open scoped TensorProduct
18 
19 universe u
20 
21 attribute [local instance] HasDerivedCategory.standard
22 
23 namespace PaperXII.HeckeCarriers
24 
25 /-- An ordinary carrier is an actual finite module. -/
26 structure FiniteModule (R : Type u) [CommRing R] where
27   object : ModuleCat.{u} R
28   finite : Module.Finite R object
29 
30 attribute [instance] FiniteModule.finite
31 
32 /-- The ordinary and perfect derived alternatives retain their actual objects. -/
33 def Carrier (R : Type u) [CommRing R] :=
34   FiniteModule R ⊕ PerfectDerivedSupport.PerfectComplex R
35 
36 variable {R S T E : Type u} [CommRing R] [CommRing S] [CommRing T] [Field E]
37 
38 /-- Ordinary fibers have one degree; derived fibers have integer degrees. -/
39 def Carrier.Degree : Carrier R → Type
40   | .inl _ => PUnit
41   | .inr _ => ℤ
42 
43 /-- The actual support of the underlying ordinary or perfect derived object. -/
44 def support : Carrier R → Set (PrimeSpectrum R)
45   | .inl M => Module.support R M.object
46   | .inr C => PerfectDerivedSupport.support C
47 
48 /-- Full support is equality with the entire prime spectrum. -/
49 def FullSupport (C : Carrier R) : Prop := support C = Set.univ
50 
51 /-- Ordinary tensor fibers and actual derived cohomology of specialized objects. -/
52 def fiberSpace (C : Carrier R) (y : R →+* E) : C.Degree → ModuleCat.{u} E :=
53   match C with
54   | .inl M => fun _ => (ModuleCat.extendScalars y).obj M.object
55   | .inr P => fun n => PerfectCohomology.cohomology (P.baseChange y) n
56 
57 /-- Literal nonvanishing of the tensor module or the specialized derived object. -/
58 def FiberNonzero (C : Carrier R) (y : R →+* E) : Prop :=
59   match C with
60   | .inl M => ¬IsZero ((ModuleCat.extendScalars y).obj M.object)
61   | .inr P => ¬IsZero (P.baseChange y).object
62 
63 /-- The operator is induced from multiplication on the original module or complex. -/
64 def heckeOperator (C : Carrier R) (y : R →+* E) :
65     (n : C.Degree) → R → (fiberSpace C y n ⟶ fiberSpace C y n) :=
66   match C with
67   | .inl M => fun _ r => (ModuleCat.extendScalars y).map (r • 𝟙 M.object)
68   | .inr P => fun n r => DerivedHeckeAction.perfectCohomologyOperator P y n r
69 
70 /-- Both actual constructions satisfy the tensor scalar identity. -/
71 theorem heckeOperator_eq_scalar (C : Carrier R) (y : R →+* E)
72     (n : C.Degree) (r : R) :
73     heckeOperator C y n r = y r • 𝟙 (fiberSpace C y n) := by
74   cases C with
75   | inl M => exact DerivedHeckeAction.extendScalars_smul_id y M.object r
76   | inr P => exact DerivedHeckeAction.perfectCohomologyOperator_eq_scalar P y n r
77 
78 /-- The tensor scalar identity on each actual vector. -/
79 theorem heckeOperator_apply (C : Carrier R) (y : R →+* E)
80     (n : C.Degree) (r : R) (z : fiberSpace C y n) :
81     heckeOperator C y n r z = y r • z := by
82   rw [heckeOperator_eq_scalar]
83   rfl
84 
85 /-- A common eigenvector is a nonzero vector with all prescribed eigenvalues. -/
86 def IsEigenvector (C : Carrier R) (y : R →+* E) (n : C.Degree)
87     (z : fiberSpace C y n) : Prop :=
88   z ≠ 0 ∧ ∀ r : R, heckeOperator C y n r z = y r • z
89 
90 /-- Every nonzero vector has the eigenvalues of the specialized point. -/
91 theorem isEigenvector_of_ne_zero (C : Carrier R) (y : R →+* E)
92     (n : C.Degree) (z : fiberSpace C y n) (hz : z ≠ 0) :
93     IsEigenvector C y n z :=
94   ⟨hz, fun r => heckeOperator_apply C y n r z⟩
95 
96 /-- The actual bounded model interval, with the sole ordinary degree allowed. -/
97 def DegreeRange (C : Carrier R) : C.Degree → Prop :=
98   match C with
99   | .inl _ => fun _ => True
100   | .inr P => fun (n : ℤ) => P.model.lower ≤ n ∧ n ≤ P.model.upper
101 
102 /-- A supported point supplies a nonzero actual eigensystem in the model range. -/
103 theorem supported_point_eigensystem_in_range (C : Carrier R) (y : R →+* E)
104     (hy : FieldFibers.pointPrime y ∈ support C) :
105     ∃ n : C.Degree, DegreeRange C n ∧
106       ∃ z : fiberSpace C y n, IsEigenvector C y n z := by
107   cases C with
108   | inl M =>
109     let : Algebra R E := y.toAlgebra
110     have : Nontrivial (E ⊗[R] M.object) :=
111       (FieldFibers.nontrivial_fiber_iff_support (M := M.object) y).mpr hy
112     obtain ⟨z, hz⟩ := exists_ne (0 : E ⊗[R] M.object)
113     exact ⟨PUnit.unit, trivial, z, isEigenvector_of_ne_zero (.inl M) y _ z hz⟩
114   | inr P =>
115     have hP := (PerfectDerivedSupport.nonzero_fiber_iff_support P y).mpr hy
116     obtain ⟨n, hlo, hhi, z, hz⟩ :=
117       PerfectCohomology.exists_nonzero_vector_in_range P y hP
118     exact ⟨n, ⟨hlo, hhi⟩, z, isEigenvector_of_ne_zero (.inr P) y n z hz⟩
119 
120 /-- A supported point supplies an actual nonzero eigenvector. -/
121 theorem supported_point_eigensystem (C : Carrier R) (y : R →+* E)
122     (hy : FieldFibers.pointPrime y ∈ support C) :
123     ∃ n : C.Degree, ∃ z : fiberSpace C y n, IsEigenvector C y n z := by
124   obtain ⟨n, _, z, hz⟩ := supported_point_eigensystem_in_range C y hy
125   exact ⟨n, z, hz⟩
126 
127 /-- Support implies literal nonvanishing of the actual ordinary or derived fiber. -/
128 theorem supported_point_fiber_nonzero (C : Carrier R) (y : R →+* E)
129     (hy : FieldFibers.pointPrime y ∈ support C) : FiberNonzero C y := by
130   cases C with
131   | inl M =>
132     obtain ⟨n, z, hz⟩ := supported_point_eigensystem (.inl M) y hy
133     intro hzero
134     have hsub : Subsingleton ((ModuleCat.extendScalars y).obj M.object) :=
135       ModuleCat.isZero_iff_subsingleton.mp hzero
136     exact hz.1 (hsub.elim z 0)
137   | inr P => exact (PerfectDerivedSupport.nonzero_fiber_iff_support P y).mpr hy
138 
139 /-- Full support provides an eigensystem at every field-valued point. -/
140 theorem fullSupport_eigensystem_in_range (C : Carrier R) (y : R →+* E)
141     (hC : FullSupport C) :
142     ∃ n : C.Degree, DegreeRange C n ∧
143       ∃ z : fiberSpace C y n, IsEigenvector C y n z := by
144   apply supported_point_eigensystem_in_range C y
145   rw [hC]
146   trivial
147 
148 /-- The comparison hypothesis is the actual inverse-image support inclusion. -/
149 def SupportComparison (f : R →+* T) (M : Carrier R) (H : Carrier T) : Prop :=
150   PrimeSpectrum.comap f ⁻¹' support M ⊆ support H
151 
152 /-- Pullback of the prime kernel agrees with composition of field-valued points. -/
153 theorem pointPrime_comp (f : R →+* T) (y : T →+* E) :
154     PrimeSpectrum.comap f (FieldFibers.pointPrime y) =
155       FieldFibers.pointPrime (y.comp f) := by
156   ext r
157   rfl
158 
159 /-- A compatible point inherits support through the literal support comparison. -/
160 theorem supportComparison_pointwise (f : R →+* T) (M : Carrier R) (H : Carrier T)
161     (comparison : SupportComparison f M H) (x : R →+* E) (y : T →+* E)
162     (hcomp : y.comp f = x) (hx : FieldFibers.pointPrime x ∈ support M) :
163     FieldFibers.pointPrime y ∈ support H := by
164   apply comparison
165   change PrimeSpectrum.comap f (FieldFibers.pointPrime y) ∈ support M
166   rw [pointPrime_comp, hcomp]
167   exact hx
168 
169 /-- The actual support inclusion transports literal fiber nonvanishing. -/
170 theorem supportComparison_pointwise_fiber_nonzero
171     (f : R →+* T) (M : Carrier R) (H : Carrier T)
172     (comparison : SupportComparison f M H) (x : R →+* E) (y : T →+* E)
173     (hcomp : y.comp f = x) (hx : FieldFibers.pointPrime x ∈ support M) :
174     FiberNonzero H y :=
175   supported_point_fiber_nonzero H y
176     (supportComparison_pointwise f M H comparison x y hcomp hx)
177 
178 /-- Full support transports through the actual comparison. -/
179 theorem supportComparison_fullSupport (f : R →+* T) (M : Carrier R) (H : Carrier T)
180     (comparison : SupportComparison f M H) (hM : FullSupport M) : FullSupport H := by
181   apply Set.eq_univ_of_forall
182   intro q
183   apply comparison
184   change PrimeSpectrum.comap f q ∈ support M
185   rw [hM]
186   trivial
187 
188 /-- The comparison gives a nonzero actual Hecke eigenvector at every compatible point. -/
189 theorem supportComparison_pointwise_eigensystem
190     (f : R →+* T) (M : Carrier R) (H : Carrier T)
191     (comparison : SupportComparison f M H) (x : R →+* E) (y : T →+* E)
192     (hcomp : y.comp f = x) (hx : FieldFibers.pointPrime x ∈ support M) :
193     ∃ n : H.Degree, DegreeRange H n ∧
194       ∃ z : fiberSpace H y n, IsEigenvector H y n z :=
195   supported_point_eigensystem_in_range H y
196     (supportComparison_pointwise f M H comparison x y hcomp hx)
197 
198 /-- Actual scalar extension of a finite ordinary module. -/
199 def FiniteModule.baseChange (M : FiniteModule R) (f : R →+* S) : FiniteModule S :=
200   ⟨(ModuleCat.extendScalars f).obj M.object,
201     PerfectModels.finite_extendScalars f M.object⟩
202 
203 /-- Actual ordinary or derived scalar extension, preserving the carrier kind. -/
204 def Carrier.baseChange (C : Carrier R) (f : R →+* S) : Carrier S :=
205   match C with
206   | .inl M => .inl (M.baseChange f)
207   | .inr P => .inr (P.baseChange f)
208 
209 /-- Both actual scalar extensions have exactly the spectral inverse-image support. -/
210 theorem support_baseChange (C : Carrier R) (f : R →+* S) :
211     support (C.baseChange f) = PrimeSpectrum.comap f ⁻¹' support C := by
212   cases C with
213   | inl M =>
214     let : Algebra R S := f.toAlgebra
215     exact BaseChangeSupport.support_baseChange (R := R) (S := S) (M := M.object)
216   | inr P => exact PerfectDerivedSupport.support_baseChange P f
217 
218 /-- Actual scalar extension constructs the required support comparison. -/
219 theorem supportComparison_baseChange (C : Carrier R) (f : R →+* S) :
220     SupportComparison f C (C.baseChange f) := by
221   unfold SupportComparison
222   rw [support_baseChange]
223 
224 /-- Full support is preserved by either actual scalar extension. -/
225 theorem fullSupport_baseChange (C : Carrier R) (f : R →+* S) (hC : FullSupport C) :
226     FullSupport (C.baseChange f) :=
227   supportComparison_fullSupport f C (C.baseChange f) (supportComparison_baseChange C f) hC
228 
229 /-- Ring identification transports the actual support by its induced spectrum map. -/
230 theorem support_ringEquiv (C : Carrier R) (e : R ≃+* S) :
231     PrimeSpectrum.comap e.toRingHom '' support (C.baseChange e.toRingHom) = support C := by
232   rw [support_baseChange, Set.image_preimage_eq_inter_range]
233   have hsurj : Function.Surjective (PrimeSpectrum.comap e.toRingHom) :=
234     (PrimeSpectrum.isHomeomorph_comap_of_bijective e.bijective).surjective
235   rw [Set.range_eq_univ.mpr hsurj, Set.inter_univ]
236 
237 end PaperXII.HeckeCarriers

Back to source controls