PerfectDerivedSupport.lean

1 import PaperXII.PerfectModels
2 import PaperXII.ComplexSupport
3 import Mathlib.RingTheory.Spectrum.Prime.Topology
4 
5 /-!
6 # Intrinsic derived support of perfect objects
7 
8 A perfect object is an actual object of Mathlib's derived category equipped
9 with a bounded finite-projective model and an actual derived isomorphism.
10 Every scalar specialization and support assertion is invariant under changing
11 that model or replacing the derived object by an isomorphic one.
12 -/
13 
14 noncomputable section
15 
16 open CategoryTheory CategoryTheory.Limits
17 
18 universe u
19 
20 attribute [local instance] HasDerivedCategory.standard
21 
22 namespace PaperXII.PerfectDerivedSupport
23 
24 open PerfectModels
25 
26 /-- An arbitrary perfect derived object with a bounded finite-projective model. -/
27 structure PerfectComplex (R : Type u) [CommRing R] where
28   object : DerivedCategory (ModuleCat.{u} R)
29   model : PerfectModel R
30   modelIso : model.derivedObject ≅ object
31 
32 variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
33 
34 /-- A bounded projective model determines a perfect derived object. -/
35 def ofModel (P : PerfectModel R) : PerfectComplex R :=
36   ⟨P.derivedObject, P, Iso.refl _⟩
37 
38 /-- Derived scalar extension, computed on the finite-projective model. -/
39 def PerfectComplex.baseChange (P : PerfectComplex R) (f : R →+* S) : PerfectComplex S :=
40   ofModel (P.model.baseChange f)
41 
42 /-- Every actual derived isomorphism induces one after arbitrary scalar extension. -/
43 def baseChangeIso (f : R →+* S) {P Q : PerfectComplex R}
44     (e : P.object ≅ Q.object) : (P.baseChange f).object ≅ (Q.baseChange f).object :=
45   baseChange_derivedIso f P.model Q.model (P.modelIso ≪≫ e ≪≫ Q.modelIso.symm)
46 
47 /-- Successive derived scalar extensions agree with extension by the composite. -/
48 def baseChangeCompIso (P : PerfectComplex R) (f : R →+* S) (g : S →+* T) :
49     ((P.baseChange f).baseChange g).object ≅ (P.baseChange (g.comp f)).object :=
50   ComplexSupport.fiberCompIso f g P.model.complex
51 
52 /-- Identity scalar extension recovers the arbitrary represented derived object. -/
53 def baseChangeIdIso (P : PerfectComplex R) :
54     (P.baseChange (RingHom.id R)).object ≅ P.object :=
55   DerivedCategory.Q.mapIso (ComplexBaseChange.baseChangeIdIso P.model.complex) ≪≫ P.modelIso
56 
57 /-- The residue-field definition of derived support in the original manuscript. -/
58 def support (P : PerfectComplex R) : Set (PrimeSpectrum R) :=
59   ComplexSupport.support P.model.complex
60 
61 /-- Full support of a perfect derived object. -/
62 def FullSupport (P : PerfectComplex R) : Prop := support P = Set.univ
63 
64 /-- Derived support is independent of both model and representative. -/
65 theorem support_eq_of_iso {P Q : PerfectComplex R} (e : P.object ≅ Q.object) :
66     support P = support Q := by
67   ext p
68   exact not_congr (baseChangeIso (algebraMap R p.asIdeal.ResidueField) e).isZero_iff
69 
70 /-- The field-valued criterion uses the exact prime kernel of the point. -/
71 theorem nonzero_fiber_iff_support {K : Type u} [Field K] (P : PerfectComplex R)
72     (x : R →+* K) :
73     ¬IsZero (P.baseChange x).object ↔ FieldFibers.pointPrime x ∈ support P :=
74   ComplexSupport.nonzero_fiber_iff_support x P.model.complex
75 
76 /-- Derived support under every scalar map is the actual spectral inverse image. -/
77 theorem support_baseChange (P : PerfectComplex R) (f : R →+* S) :
78     support (P.baseChange f) = PrimeSpectrum.comap f ⁻¹' support P :=
79   ComplexSupport.support_baseChange f P.model.complex
80 
81 /-- Original Theorem 6.16, in literal ambient-spectrum form for the actual quotient. -/
82 theorem derived_quotient_support (P : PerfectComplex R) (I : Ideal R) :
83     PrimeSpectrum.comap (Ideal.Quotient.mk I) '' support (P.baseChange (Ideal.Quotient.mk I)) =
84       support P ∩ PrimeSpectrum.zeroLocus I :=
85   ComplexSupport.image_support_quotient I P.model.complex
86 
87 /-- Support transports along a ring isomorphism by its actual map on spectra. -/
88 theorem support_ringEquiv (P : PerfectComplex R) (e : R ≃+* S) :
89     PrimeSpectrum.comap e.toRingHom '' support (P.baseChange e.toRingHom) = support P := by
90   rw [support_baseChange, Set.image_preimage_eq_inter_range]
91   have hsurj : Function.Surjective (PrimeSpectrum.comap e.toRingHom) :=
92     (PrimeSpectrum.isHomeomorph_comap_of_bijective e.bijective).surjective
93   rw [Set.range_eq_univ.mpr hsurj, Set.inter_univ]
94 
95 /-- Full support survives arbitrary derived scalar extension. -/
96 theorem fullSupport_baseChange (P : PerfectComplex R) (f : R →+* S)
97     (h : FullSupport P) : FullSupport (P.baseChange f) :=
98   ComplexSupport.fullSupport_baseChange f P.model.complex h
99 
100 /-- Every field-valued fiber of a full-support perfect complex is nonzero. -/
101 theorem nonzero_fiber_of_fullSupport {K : Type u} [Field K] (P : PerfectComplex R)
102     (x : R →+* K) (h : FullSupport P) : ¬IsZero (P.baseChange x).object :=
103   ComplexSupport.nonzero_fiber_of_fullSupport x P.model.complex h
104 
105 /-- The actual derived cohomology functors detect nonzero field fibers. -/
106 theorem exists_nonzero_cohomology {K : Type u} [Field K] (P : PerfectComplex R)
107     (x : R →+* K) (h : ¬IsZero (P.baseChange x).object) :
108     ∃ n : ℤ, ¬IsZero ((DerivedCategory.homologyFunctor (ModuleCat K) n).obj
109       (P.baseChange x).object) := by
110   contrapose! h
111   exact (ComplexFieldFibers.derived_isZero_iff_homology _).mpr h
112 
113 /-- A surviving actual cochain cohomology object witnesses the same derived fiber. -/
114 theorem exists_nonzero_model_cohomology {K : Type u} [Field K] (P : PerfectComplex R)
115     (x : R →+* K) (h : ¬IsZero (P.baseChange x).object) :
116     ∃ n : ℤ, ¬IsZero ((P.baseChange x).model.complex.homology n) :=
117   ComplexFieldFibers.exists_nonzero_homology_of_not_isZero _ h
118 
119 end PaperXII.PerfectDerivedSupport

Back to source controls