Documentation

TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.Basic

Finitely presented sheaves on schemes #

This file packages Mathlib's finite-presentation condition for sheaves of modules as a full subcategory on an arbitrary scheme. On a locally Noetherian scheme this supplies the objects used in the standard coherent-sheaf notion.

The main declarations are:

The inclusion uses the site-level theorem that an invertible sheaf is finitely presented: its rank-one local trivializations give finite generators and have no relations. Thus the existing Layer A line-bundle objects can be consumed by the coherent-cohomology theory planned in Layer B.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer B, item "Coherent sheaves and cohomology Hⁱ(X, ℱ)", while supplying the direct bridge from Layer A's invertible sheaves. No formalization is vendored. The definition reuses Mathlib's SheafOfModules.IsFinitePresentation and ObjectProperty.FullSubcategory.

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

The full category of finitely presented sheaves of modules on a scheme.

Equations
Instances For
    source
    instance TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.instIsFinitePresentationOpensCarrierCarrierCommRingCatObjSheafOfModulesRingCatSheafIsFinitePresentation {X : AlgebraicGeometry.Scheme} (F : FinitelyPresentedSheaf X) :
    F.obj.IsFinitePresentation

    The underlying sheaf of a finitely presented sheaf is finitely presented.

    source
    @[reducible, inline]
    abbrev TauCeti.AlgebraicGeometry.InvertibleSheaf.toFinitelyPresented (X : AlgebraicGeometry.Scheme) :
    CategoryTheory.Functor (InvertibleSheaf X) (FinitelyPresentedSheaf X)

    The fully faithful inclusion of invertible sheaves into finitely presented sheaves.

    Equations
    Instances For