PerfectCohomology.lean

1 import PaperXII.PerfectDerivedSupport
2 
3 /-!
4 # Cohomological range of perfect scalar specializations
5 
6 The endpoints are the actual bounds of a bounded finite-projective model.
7 Vanishing is transported to the arbitrary represented derived object through
8 its model isomorphism. After any scalar extension the same endpoints bound
9 the actual derived cohomology. A nonzero fiber therefore contains a nonzero
10 cohomology vector in that interval.
11 -/
12 
13 noncomputable section
14 
15 open CategoryTheory CategoryTheory.Limits
16 
17 universe u
18 
19 attribute [local instance] HasDerivedCategory.standard
20 
21 namespace PaperXII.PerfectCohomology
22 
23 open PerfectDerivedSupport
24 
25 variable {R S : Type u} [CommRing R] [CommRing S]
26 
27 /-- The actual module-valued derived cohomology of the represented object. -/
28 abbrev cohomology (P : PerfectComplex R) (n : ℤ) : ModuleCat.{u} R :=
29   (DerivedCategory.homologyFunctor (ModuleCat R) n).obj P.object
30 
31 /-- The represented derived cohomology agrees with that of its chosen model. -/
32 def cohomologyModelIso (P : PerfectComplex R) (n : ℤ) :
33     cohomology P n ≅ P.model.complex.homology n :=
34   (DerivedCategory.homologyFunctor (ModuleCat R) n).mapIso P.modelIso.symm ≪≫
35     (DerivedCategory.homologyFunctorFactors (ModuleCat R) n).app P.model.complex
36 
37 /-- Actual derived cohomology vanishes below the model's lower bound. -/
38 theorem isZero_cohomology_below (P : PerfectComplex R) (n : ℤ)
39     (hn : n < P.model.lower) : IsZero (cohomology P n) :=
40   (P.model.complex.isZero_of_isGE P.model.lower n hn).of_iso (cohomologyModelIso P n)
41 
42 /-- Actual derived cohomology vanishes above the model's upper bound. -/
43 theorem isZero_cohomology_above (P : PerfectComplex R) (n : ℤ)
44     (hn : P.model.upper < n) : IsZero (cohomology P n) :=
45   (P.model.complex.isZero_of_isLE P.model.upper n hn).of_iso (cohomologyModelIso P n)
46 
47 /-- Every nonzero actual cohomology object lies in the model's closed interval. -/
48 theorem cohomology_degree_bounds (P : PerfectComplex R) (n : ℤ)
49     (hn : ¬IsZero (cohomology P n)) : P.model.lower ≤ n ∧ n ≤ P.model.upper := by
50   constructor
51   · by_contra h
52     exact hn (isZero_cohomology_below P n (lt_of_not_ge h))
53   · by_contra h
54     exact hn (isZero_cohomology_above P n (lt_of_not_ge h))
55 
56 /-- Scalar extension keeps the lower cohomological bound without a flatness assumption. -/
57 theorem isZero_baseChange_cohomology_below (P : PerfectComplex R) (f : R →+* S)
58     (n : ℤ) (hn : n < P.model.lower) : IsZero (cohomology (P.baseChange f) n) :=
59   isZero_cohomology_below (P.baseChange f) n hn
60 
61 /-- Scalar extension keeps the upper cohomological bound without a flatness assumption. -/
62 theorem isZero_baseChange_cohomology_above (P : PerfectComplex R) (f : R →+* S)
63     (n : ℤ) (hn : P.model.upper < n) : IsZero (cohomology (P.baseChange f) n) :=
64   isZero_cohomology_above (P.baseChange f) n hn
65 
66 /-- Every surviving specialized degree is in the original model's interval. -/
67 theorem baseChange_cohomology_degree_bounds (P : PerfectComplex R) (f : R →+* S)
68     (n : ℤ) (hn : ¬IsZero (cohomology (P.baseChange f) n)) :
69     P.model.lower ≤ n ∧ n ≤ P.model.upper :=
70   cohomology_degree_bounds (P.baseChange f) n hn
71 
72 /-- A nonzero module object has an actual nonzero element. -/
73 theorem exists_nonzero_vector (M : ModuleCat.{u} R) (h : ¬IsZero M) :
74     ∃ v : M, v ≠ 0 := by
75   by_contra! hv
76   apply h
77   rw [ModuleCat.isZero_iff_subsingleton]
78   exact ⟨fun a b => (hv a).trans (hv b).symm⟩
79 
80 /-- A nonzero specialized derived object has cohomology in the bounded interval. -/
81 theorem exists_nonzero_cohomology_in_range (P : PerfectComplex R) (f : R →+* S)
82     (h : ¬IsZero (P.baseChange f).object) :
83     ∃ n : ℤ, P.model.lower ≤ n ∧ n ≤ P.model.upper ∧
84       ¬IsZero (cohomology (P.baseChange f) n) := by
85   have hex : ∃ n : ℤ, ¬IsZero (cohomology (P.baseChange f) n) := by
86     contrapose! h
87     exact (ComplexFieldFibers.derived_isZero_iff_homology _).mpr h
88   obtain ⟨n, hn⟩ := hex
89   obtain ⟨hlo, hhi⟩ := baseChange_cohomology_degree_bounds P f n hn
90   exact ⟨n, hlo, hhi, hn⟩
91 
92 /-- A surviving scalar specialization gives a nonzero actual cohomology vector
93 in a degree bounded by the original finite-projective model. -/
94 theorem exists_nonzero_vector_in_range (P : PerfectComplex R) (f : R →+* S)
95     (h : ¬IsZero (P.baseChange f).object) :
96     ∃ (n : ℤ), P.model.lower ≤ n ∧ n ≤ P.model.upper ∧
97       ∃ v : cohomology (P.baseChange f) n, v ≠ 0 := by
98   obtain ⟨n, hlo, hhi, hn⟩ := exists_nonzero_cohomology_in_range P f h
99   exact ⟨n, hlo, hhi, exists_nonzero_vector _ hn⟩
100 
101 /-- Every field-valued point of a full-support perfect complex has such a vector. -/
102 theorem exists_nonzero_fiber_vector_in_range {K : Type u} [Field K]
103     (P : PerfectComplex R) (x : R →+* K) (h : FullSupport P) :
104     ∃ (n : ℤ), P.model.lower ≤ n ∧ n ≤ P.model.upper ∧
105       ∃ v : cohomology (P.baseChange x) n, v ≠ 0 :=
106   exists_nonzero_vector_in_range P x (nonzero_fiber_of_fullSupport P x h)
107 
108 end PaperXII.PerfectCohomology

Back to source controls