Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Families.Scheme

Scheme-indexed triangulated families #

This file specializes the generic categorical family interface to the category of schemes over a fixed scheme. The fibers and pullback functors remain client-supplied categorical data; no stability condition is imposed.

source
@[reducible, inline]
abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange (S : Scheme) :
Type (u + 1)

The category of scheme-valued base changes over a fixed scheme.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily (S : Scheme) :
    Type (max (u + 1) (u_1 + 1))

    An abstract triangulated category over every scheme base change of S. The fibers and pullback functors are explicit client data.

    Equations
    Instances For
      source
      def AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant (S : Scheme) (C : Type w) [CategoryTheory.Category.{w, w} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] :
      SchemeTriangulatedFiberFamily S

      The constant triangulated family on the category of schemes over S.

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