Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Basic

Derived categories of module sheaves on schemes #

For a scheme X, Mathlib's abelian category X.Modules supplies the generic derived category and its bounded subcategory. This module records those scheme-specific specializations without introducing a second derived-category construction.

The chosen localization #

Mathlib's HasDerivedCategory C records a chosen localization at the quasi-isomorphisms, and its guidance is that the standard large localization HasDerivedCategory.standard C be introduced locally where a construction needs it, never registered globally. There is therefore no global instance here: this file and every geometric consumer that spells a derived category declare attribute [local instance] HasDerivedCategory.standard after their preamble, so that the instance argument elaborated into every signature is literally HasDerivedCategory.standard _ and agrees across files and across the two spellings X.Modules and SheafOfModules X.ringCatSheaf, which are reducibly equal. A consumer that wants a different localization takes [HasDerivedCategory C] as a hypothesis instead.

source
@[reducible, inline]
abbrev AlgebraicGeometry.DerivedCategory.SchemeDerivedCategory (X : Scheme) :
Type (u + 1)

The derived category of sheaves of modules on a scheme, constructed using Mathlib's standard localization at quasi-isomorphisms.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.DerivedCategory.SchemeBoundedDerivedCategory (X : Scheme) :
    Type (u + 1)

    The bounded derived category of sheaves of modules on a scheme, defined using the canonical t-structure on SchemeDerivedCategory X.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev AlgebraicGeometry.DerivedCategory.SchemeDerivedCategory.Q (X : Scheme) :
      CategoryTheory.Functor (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)

      The localization functor from cochain complexes of module sheaves to the scheme's derived category.

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev AlgebraicGeometry.DerivedCategory.SchemeDerivedCategory.boundedInclusion (X : Scheme) :
        CategoryTheory.Functor (SchemeBoundedDerivedCategory X) (SchemeDerivedCategory X)

        The canonical inclusion of the bounded derived category into the unbounded derived category.

        Equations
        Instances For