Documentation

TauCeti.AlgebraicGeometry.VectorBundle.Quasicoherent

Finite locally free sheaves as quasicoherent sheaves #

Finite locally free sheaves on a scheme embed fully faithfully into the symmetric monoidal category of quasicoherent sheaves by a symmetric monoidal functor.

Main declarations #

source
@[reducible, inline]
abbrev TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.toQuasicoherent (X : AlgebraicGeometry.Scheme) :
CategoryTheory.Functor (FiniteLocallyFreeSheaf X) (QuasicoherentSheaf X)

The fully faithful symmetric monoidal inclusion of finite locally free sheaves into quasicoherent sheaves.

Equations
Instances For
    source
    instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instFullQuasicoherentSheafToQuasicoherent (X : AlgebraicGeometry.Scheme) :
    (toQuasicoherent X).Full
    source
    instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instFaithfulQuasicoherentSheafToQuasicoherent (X : AlgebraicGeometry.Scheme) :
    (toQuasicoherent X).Faithful
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.toQuasicoherent_obj_obj (X : AlgebraicGeometry.Scheme) (E : FiniteLocallyFreeSheaf X) :
    ((toQuasicoherent X).obj E).obj = E.obj
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.toQuasicoherent_map_hom (X : AlgebraicGeometry.Scheme) {E F : FiniteLocallyFreeSheaf X} (f : E ⟶ F) :
    ((toQuasicoherent X).map f).hom = f.hom