Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Basic.Definitions

Definitions for coherent sheaves on a scheme #

Layer B, stage 1. Mathlib already supplies the abelian category X.Modules of sheaves of modules on a scheme X, together with SheafOfModules.IsQuasicoherent and SheafOfModules.IsFinitePresentation. What is missing is coherence and the category Coh X; this file adds them.

Definition used #

On a locally noetherian scheme, Serre's condition (finite type, and every locally finitely generated subsheaf of every restriction is finitely presented) is equivalent to finite presentation. Since the target of this development is smooth projective varieties over a field — always noetherian — IsCoherent is defined as finite presentation.

That is a genuine restriction of generality, recorded here rather than hidden: on a non-noetherian scheme this definition is finite presentation, which is strictly stronger than Serre-coherence. Do not use Coh outside the locally noetherian setting without revisiting this.

Stage 1 status #

Coh X is defined here and inherits its category structure. Closure under kernels and cokernels in X.Modules is proved in DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Abelian.Kernels. Generic finite-presentation closure under extensions is proved in DerivedAlgGeo.Algebra.Category.ModuleCat.Sheaf.Presentation.Extensions, and its coherent specialization is installed by DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Abelian.Extensions. The module DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Abelian.Basic installs the abelian instance and packages the inclusion as an exact functor.

The affine equivalence Coh (Spec R) ≌ FGModuleCat R is proved in DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Affine.Comparison.

Downstream developments should import DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Abelian.Basic for the completed stage-1 API.

References #

source
def AlgebraicGeometry.Scheme.Modules.IsCoherent (X : Scheme) (M : X.Modules) :
Prop

A sheaf of modules on a scheme is coherent when it is of finite presentation.

On a locally noetherian scheme this agrees with Serre's condition; see the module docstring for the caveat outside that setting.

Equations
Instances For
    source
    def AlgebraicGeometry.Scheme.coherent (X : Scheme) :
    CategoryTheory.ObjectProperty X.Modules

    Coherence, packaged as an ObjectProperty so that Coh X can be carved out as a full subcategory of X.Modules.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Scheme.coherent_iff (X : Scheme) (M : X.Modules) :
      X.coherent M ↔ Modules.IsCoherent X M
      source
      def AlgebraicGeometry.Coh (X : Scheme) :
      Type (u + 1)

      The category Coh X of coherent sheaves on a scheme X, as a full subcategory of X.Modules.

      Intended for locally noetherian X; the typeclass assumption is not imposed on the definition itself so that the inclusion functor is available unconditionally.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance AlgebraicGeometry.Coh.instCategory (X : Scheme) :
        CategoryTheory.Category.{u, u + 1} (Coh X)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def AlgebraicGeometry.Coh.ι (X : Scheme) :
        CategoryTheory.Functor (Coh X) X.Modules

        The inclusion Coh X ⥤ X.Modules.

        Equations
        Instances For
          source
          instance AlgebraicGeometry.Coh.full_ι (X : Scheme) :
          (ι X).Full

          The inclusion of coherent sheaves is full. Stated on Coh.ι itself, not inherited: ι is a def, so instance search does not unfold it to reach ObjectProperty.full_ι. Together with Coh.faithful_ι this makes Coh.ι reflect finite limits and colimits (fullyFaithful_reflectsLimits), which is what preservesFiniteLimits_of_reflects_of_preserves needs to transfer exactness along the inclusion, as Coh.pushforward does.

          source
          instance AlgebraicGeometry.Coh.faithful_ι (X : Scheme) :
          (ι X).Faithful

          The inclusion of coherent sheaves is faithful; see Coh.full_ι for why this is stated on Coh.ι rather than inherited.