Bounded coherent and perfect derived categories in scheme families

The canonical geometric categories D(Coh X), Dᵇ(Coh X), and Perf(X) live in DerivedCategory/Coherent.lean. This file evaluates them on scheme base changes and records the contract needed to lift coherent pullback to the bounded subcategory.

Coherence is preserved by every pullback (Coh.pullback, in Modules/Coherent/Pullback.lean), but exactness of the pullback is not, so the contract HasCoherentPullback records it and the bounded lift is constructed only from an instance; Families/CoherentPullback.lean discharges the contract for exact, in particular flat, pullback. Preservation of the perfect envelope is a theorem for every instance; the perfect lift lives in Families/PerfectPullback.lean, and the identity and composition laws of the bounded and perfect lifts, theorems for every instance, in Families/CoherentPullbackCoherence.lean. No geometric slicing, openness, relative-HN existence, moduli theorem, or conclusion of Theorem 22.2 is asserted.

Main definitions

• SchemeBaseChange.BoundedCoherentDerivedFiber, SchemeBaseChange.PerfectDerivedFiber, and their residue-field forms;
• SchemeBaseChange.HasCoherentPullback, with HasCoherentPullback.ofExactSheafPullback, the constructor every degreewise inhabitant should use;
• SchemeBaseChange.coherentDerivedPullback, SchemeBaseChange.boundedCoherentDerivedPullback, and SchemeBaseChange.boundedCoherentDerivedPullbackCompInclusion.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentDerivedFiber {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] : Type (u + 1)

The bounded coherent derived fiber over a locally Noetherian scheme base change.

Equations

• T.BoundedCoherentDerivedFiber = AlgebraicGeometry.DerivedCategory.SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left T)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PerfectDerivedFiber {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] : Type (u + 1)

The perfect derived fiber over a locally Noetherian scheme base change.

Equations

• T.PerfectDerivedFiber = AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory (CategoryTheory.Over.left T)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.ResidueBoundedCoherentDerivedFiber {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) [IsLocallyNoetherian (CategoryTheory.Over.left (T.residue x))] : Type (u + 1)

The bounded coherent derived category of the residue-field scheme.

Equations

• T.ResidueBoundedCoherentDerivedFiber x = (T.residue x).BoundedCoherentDerivedFiber

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.ResiduePerfectDerivedFiber {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) [IsLocallyNoetherian (CategoryTheory.Over.left (T.residue x))] : Type (u + 1)

The perfect derived category of the residue-field scheme.

Equations

• T.ResiduePerfectDerivedFiber x = (T.residue x).PerfectDerivedFiber

class AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] : Type (u + 1)

The geometric data needed to restrict module-sheaf pullback to coherent sheaves. Exactness is part of the contract; it is what makes the induced derived pullback preserve bounded objects.

• sheafPullback : CategoryTheory.Functor (Coh (CategoryTheory.Over.left U)) (Coh (CategoryTheory.Over.left T))

  Pullback on coherent sheaves.

• preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits (sheafPullback f)

  Coherent pullback preserves finite limits.

• preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits (sheafPullback f)

  Coherent pullback preserves finite colimits.

• comparison : (sheafPullback f).comp (Coh.ι (CategoryTheory.Over.left T)) ≅ (Coh.ι (CategoryTheory.Over.left U)).comp (modulePullback f)

  After forgetting coherence, this is ordinary module-sheaf pullback.

• derivedPullback : CategoryTheory.Functor (SchemeCoherentDerivedCategory (CategoryTheory.Over.left U)) (SchemeCoherentDerivedCategory (CategoryTheory.Over.left T))

  The localized pullback on coherent derived categories.

• derivedFactors : DerivedCategory.Q.comp (derivedPullback f) ≅ ((sheafPullback f).mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q

  The derived functor is induced by degreewise coherent-sheaf pullback.

• derivedAdditive : (derivedPullback f).Additive

  Derived coherent pullback is additive.

• commShift : (derivedPullback f).CommShift ℤ

  Derived coherent pullback commutes with shifts.

• isTriangulated : (derivedPullback f).IsTriangulated

  Derived coherent pullback is triangulated.

• preservesBounded (E : SchemeCoherentDerivedCategory (CategoryTheory.Over.left U)) : DerivedCategory.TStructure.t.bounded E → DerivedCategory.TStructure.t.bounded ((derivedPullback f).obj E)

  Exact coherent pullback preserves canonical boundedness.

@[reducible]

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback.ofExactSheafPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] (F : CategoryTheory.Functor (Coh (CategoryTheory.Over.left U)) (Coh (CategoryTheory.Over.left T))) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (e : F.comp (Coh.ι (CategoryTheory.Over.left T)) ≅ (Coh.ι (CategoryTheory.Over.left U)).comp (modulePullback f)) : HasCoherentPullback f

Build the contract from an exact functor on coherent sheaves that forgets to module-sheaf pullback: the derived fields are Mathlib's Functor.mapDerivedCategory of that functor with its instances, and boundedness is mapDerivedCategory_bounded. Every inhabitant whose derived pullback is the degreewise one should come through here rather than restate those fields.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : CategoryTheory.Functor (SchemeCoherentDerivedCategory (CategoryTheory.Over.left U)) (SchemeCoherentDerivedCategory (CategoryTheory.Over.left T))

Coherent-sheaf pullback on unbounded derived categories.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentDerivedPullback f = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback.derivedPullback f

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instAdditiveSchemeCoherentDerivedCategoryLeftSchemeCoherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (coherentDerivedPullback f).Additive

@[implicit_reducible]

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instCommShiftSchemeCoherentDerivedCategoryLeftSchemeCoherentDerivedPullbackInt {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (coherentDerivedPullback f).CommShift ℤ

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instIsTriangulatedSchemeCoherentDerivedCategoryLeftSchemeCoherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (coherentDerivedPullback f).IsTriangulated

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : CategoryTheory.Functor U.BoundedCoherentDerivedFiber T.BoundedCoherentDerivedFiber

Exact coherent pullback restricts canonically to Dᵇ(Coh).

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instAdditiveBoundedCoherentDerivedFiberBoundedCoherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (boundedCoherentDerivedPullback f).Additive

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instCommShiftBoundedCoherentDerivedFiberBoundedCoherentDerivedPullbackInt {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (boundedCoherentDerivedPullback f).CommShift ℤ

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instCommShiftBoundedCoherentDerivedFiberBoundedCoherentDerivedPullbackInt f = id inferInstance

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPullbackCompInclusion {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (boundedCoherentDerivedPullback f).comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp (coherentDerivedPullback f)

The bounded lift forgets to coherent derived pullback.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instCommShiftBoundedCoherentDerivedFiberDerivedCategoryCohLeftSchemeHomFunctorBoundedCoherentDerivedPullbackCompInclusionInt {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : CategoryTheory.NatTrans.CommShift (boundedCoherentDerivedPullbackCompInclusion f).hom ℤ

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instIsTriangulatedBoundedCoherentDerivedFiberBoundedCoherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] : (boundedCoherentDerivedPullback f).IsTriangulated