Derived categories attached to scheme fibers

The core specialization of Mathlib's generic derived category to X.Modules lives in AlgebraicGeometry.DerivedCategory.Basic. This file evaluates those categories on scheme base changes and their residue-field fibers and records objectwise realizations of scheme-indexed triangulated families.

These are derived categories of all sheaves of modules. No bounded coherent or perfect subcategory is identified here. Moreover, the construction is objectwise: no derived pullback functor, base-change coherence, geometric slicing witness, relative HN structure, openness, boundedness, moduli result, or conclusion of Theorem 22.2 of arXiv:1902.08184v4 is asserted.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedFiber {S : Scheme} (T : SchemeBaseChange S) : Type (u + 1)

The concrete derived category attached to a scheme base change.

Equations

• T.DerivedFiber = AlgebraicGeometry.DerivedCategory.SchemeDerivedCategory (CategoryTheory.Over.left T)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedDerivedFiber {S : Scheme} (T : SchemeBaseChange S) : Type (u + 1)

The concrete bounded derived category attached to a scheme base change.

Equations

• T.BoundedDerivedFiber = AlgebraicGeometry.DerivedCategory.SchemeBoundedDerivedCategory (CategoryTheory.Over.left T)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.ResidueDerivedFiber {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : Type (u + 1)

The concrete derived category over the residue-field scheme at x.

Equations

• T.ResidueDerivedFiber x = (T.residue x).DerivedFiber

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.ResidueBoundedDerivedFiber {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : Type (u + 1)

The concrete bounded derived category over the residue-field scheme at x.

Equations

• T.ResidueBoundedDerivedFiber x = (T.residue x).BoundedDerivedFiber

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residueDerivedFiber_eq {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : T.ResidueDerivedFiber x = SchemeDerivedCategory (Spec ((CategoryTheory.Over.left T).residueField x))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residueBoundedDerivedFiber_eq {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : T.ResidueBoundedDerivedFiber x = SchemeBoundedDerivedCategory (Spec ((CategoryTheory.Over.left T).residueField x))

structure AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.DerivedRealization {S : Scheme} (F : SchemeTriangulatedFiberFamily S) : Type (max (u + 1) u_1)

Objectwise identification of a supplied triangulated family with the concrete derived categories of module sheaves. This records no compatibility between the equivalences and the supplied pullback functors.

• fiberEquivalence (T : SchemeBaseChange S) : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T ≌ T.DerivedFiber

  Equivalence between each supplied fiber and the concrete derived category on its underlying scheme.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.BoundedDerivedRealization {S : Scheme} (F : SchemeTriangulatedFiberFamily S) : Type (max (u + 1) u_1)

Objectwise identification of a supplied triangulated family with the concrete bounded derived categories of module sheaves. Derived pullback and its coherence remain additional data.

• fiberEquivalence (T : SchemeBaseChange S) : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T ≌ T.BoundedDerivedFiber

  Equivalence between each supplied fiber and the concrete bounded derived category on its underlying scheme.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.DerivedRealization.residueFiberEquivalence {S : Scheme} {F : SchemeTriangulatedFiberFamily S} (R : F.DerivedRealization) (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : F.ResidueFiber T x ≌ T.ResidueDerivedFiber x

A derived realization specializes to the actual residue-field derived category at every point.

Equations

• R.residueFiberEquivalence T x = R.fiberEquivalence (T.residue x)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.BoundedDerivedRealization.residueFiberEquivalence {S : Scheme} {F : SchemeTriangulatedFiberFamily S} (R : F.BoundedDerivedRealization) (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : F.ResidueFiber T x ≌ T.ResidueBoundedDerivedFiber x

A bounded derived realization specializes to the actual bounded derived category of the residue-field scheme at every point.

Equations

• R.residueFiberEquivalence T x = R.fiberEquivalence (T.residue x)