Finite locally free sheaves on a scheme

A sheaf of 𝒪_X-modules on a scheme X is finite locally free if it is locally free and finitely presented (SheafOfModules.isFiniteLocallyFree). These are the sheaves of sections of algebraic vector bundles of finite rank. This file packages them as the full subcategory FiniteLocallyFreeSheaf X of X.Modules and equips it with the structure inherited from X.Modules:

• it is closed under isomorphisms, and its objects are quasi-coherent;
• it is a symmetric monoidal category, with the tensor product and unit 𝒪_X of X.Modules, and its inclusion into X.Modules is braided monoidal;
• it is an additive category: it contains the zero sheaf and is closed under direct sums, so it has finite biproducts, computed in X.Modules;
• it is stable under pullback along an arbitrary morphism of schemes f : X ⟶ Y, giving the pullback functor FiniteLocallyFreeSheaf Y ⥤ FiniteLocallyFreeSheaf X.

Invertible sheaves are finite locally free, and finite locally free sheaves are finitely presented; the corresponding inclusions of full subcategories are fully faithful.

Main declarations

• AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X: finite local freeness as a property of 𝒪_X-modules;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf X: the full subcategory of finite locally free sheaves in X.Modules;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.free X I: the free sheaf on a finite type I;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullback f: the pullback of finite locally free sheaves along a morphism of schemes f;
• AlgebraicGeometry.Scheme.Modules.isMonoidal_isFiniteLocallyFree: finite local freeness is a monoidal property of 𝒪_X-modules;
• AlgebraicGeometry.Scheme.Modules.containsZero_isFiniteLocallyFree and AlgebraicGeometry.Scheme.Modules.isClosedUnderFiniteProducts_isFiniteLocallyFree, from which FiniteLocallyFreeSheaf X has finite biproducts;
• FiniteLocallyFreeSheaf.toFinitelyPresented and InvertibleSheaf.toFiniteLocallyFree: the fully faithful inclusions.

References

• The Stacks Project, Tag 01C6

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree (X : Scheme) : CategoryTheory.ObjectProperty X.Modules

Finite local freeness of 𝒪_X-modules, as a property of objects of X.Modules: an 𝒪_X-module is finite locally free if it is locally free and finitely presented.

Equations

• AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X = SheafOfModules.isFiniteLocallyFree X.ringCatSheaf

instance AlgebraicGeometry.Scheme.Modules.isClosedUnderIsomorphisms_isFiniteLocallyFree (X : Scheme) : (isFiniteLocallyFree X).IsClosedUnderIsomorphisms

Finite local freeness of 𝒪_X-modules is invariant under isomorphism.

instance AlgebraicGeometry.Scheme.Modules.isMonoidal_isFiniteLocallyFree (X : Scheme) : (isFiniteLocallyFree X).IsMonoidal

Finite local freeness is a monoidal property of 𝒪_X-modules: the structure sheaf is finite locally free, and finite locally free sheaves are closed under tensor products.

instance AlgebraicGeometry.Scheme.Modules.containsZero_isFiniteLocallyFree (X : Scheme) : (isFiniteLocallyFree X).ContainsZero

The zero 𝒪_X-module is finite locally free.

instance AlgebraicGeometry.Scheme.Modules.isClosedUnderFiniteProducts_isFiniteLocallyFree (X : Scheme) : (isFiniteLocallyFree X).IsClosedUnderFiniteProducts

Finite locally free 𝒪_X-modules are closed under finite products, which are the finite direct sums in X.Modules.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The full category of finite locally free sheaves on a scheme, that is, of locally free and finitely presented 𝒪_X-modules. Its morphisms are morphisms of 𝒪_X-modules.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf X = (AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X).FullSubcategory

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instIsLocallyFreeOpensCarrierCarrierCommRingCatObjModulesIsFiniteLocallyFree {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : SheafOfModules.IsLocallyFree E.obj

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instIsFinitePresentationOpensCarrierCarrierCommRingCatObjModulesIsFiniteLocallyFree {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : SheafOfModules.IsFinitePresentation E.obj

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instIsFiniteTypeOpensCarrierCarrierCommRingCatObjModulesIsFiniteLocallyFree {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : SheafOfModules.IsFiniteType E.obj

A finite locally free sheaf is of finite type.

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instIsQuasicoherentOpensCarrierCarrierCommRingCatObjModulesIsFiniteLocallyFree {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : SheafOfModules.IsQuasicoherent E.obj

A finite locally free sheaf is quasi-coherent.

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instHasFiniteBiproducts {X : AlgebraicGeometry.Scheme} : CategoryTheory.Limits.HasFiniteBiproducts (FiniteLocallyFreeSheaf X)

The category of finite locally free sheaves has finite biproducts, computed in X.Modules; together with its preadditive structure this makes it an additive category.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.free (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] : FiniteLocallyFreeSheaf X

The free sheaf on a finite type, as a finite locally free sheaf.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.free X I = { obj := SheafOfModules.free I, property := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.free_obj (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] : (free X I).obj = SheafOfModules.free I

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullback {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.Functor (FiniteLocallyFreeSheaf Y) (FiniteLocallyFreeSheaf X)

The pullback of finite locally free sheaves along a morphism of schemes f : X ⟶ Y: the pullback of a locally free and finitely presented 𝒪_Y-module is a locally free and finitely presented 𝒪_X-module.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullback_obj_obj {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) : ((pullback f).obj E).obj = (AlgebraicGeometry.Scheme.Modules.pullback f).obj E.obj

The underlying sheaf of the pullback of a finite locally free sheaf is its pullback as an 𝒪_Y-module.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullback_map_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {E F : FiniteLocallyFreeSheaf Y} (φ : E ⟶ F) : ((pullback f).map φ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map φ.hom) (CategoryTheory.eqToHom ⋯))

Pullback acts on a morphism of finite locally free sheaves by the underlying pullback of modules.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.toFinitelyPresented (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (FiniteLocallyFreeSheaf X) (FinitelyPresentedSheaf X)

The fully faithful inclusion of finite locally free sheaves into finitely presented sheaves.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.toFinitelyPresented X = CategoryTheory.ObjectProperty.ιOfLE ⋯

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instFullFinitelyPresentedSheafToFinitelyPresented (X : AlgebraicGeometry.Scheme) : (toFinitelyPresented X).Full

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instFaithfulFinitelyPresentedSheafToFinitelyPresented (X : AlgebraicGeometry.Scheme) : (toFinitelyPresented X).Faithful

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.InvertibleSheaf.toFiniteLocallyFree (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (InvertibleSheaf X) (FiniteLocallyFreeSheaf X)

The fully faithful inclusion of invertible sheaves into finite locally free sheaves: an invertible sheaf is locally free of rank one, hence locally free and finitely presented.

Equations

• TauCeti.AlgebraicGeometry.InvertibleSheaf.toFiniteLocallyFree X = CategoryTheory.ObjectProperty.ιOfLE ⋯

instance TauCeti.AlgebraicGeometry.instFullInvertibleSheafFiniteLocallyFreeSheafToFiniteLocallyFree (X : AlgebraicGeometry.Scheme) : (InvertibleSheaf.toFiniteLocallyFree X).Full

instance TauCeti.AlgebraicGeometry.instFaithfulInvertibleSheafFiniteLocallyFreeSheafToFiniteLocallyFree (X : AlgebraicGeometry.Scheme) : (InvertibleSheaf.toFiniteLocallyFree X).Faithful