Documentation

TauCeti.AlgebraicGeometry.Modules.Quasicoherent.Colimits

Colimits of quasicoherent sheaves #

The colimit, in the category of all sheaves of modules on a scheme, of a small diagram of quasicoherent sheaves is quasicoherent. On a spectrum it is the sheaf associated with the colimit of the modules of global sections, since the associated-sheaf functor M ↦ M~ is a left adjoint and a quasicoherent sheaf is the sheaf associated with its global sections. Restriction to an open subscheme is also a left adjoint, so restriction to affine opens gives the result on arbitrary schemes, without Noetherian or separation assumptions.

In particular direct sums of quasicoherent sheaves are quasicoherent, such as the direct sum of the homogeneous components of a graded quasicoherent algebra.

Taking sections over an affine open preserves these colimits: on Spec R, global sections restrict to an equivalence between quasicoherent sheaves and R-modules (tildeEquiv), and an affine open is the image of the affine chart Spec Γ(X, U) ⟶ X. So the sections over an affine open of a direct sum of quasicoherent sheaves are the direct sum of their sections. This fails over non-quasicompact opens, where a section of a direct sum may have infinitely many nonzero components.

Main declarations #

References #

source
theorem TauCeti.AlgebraicGeometry.isQuasicoherent_of_isColimit {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.EssentiallySmall.{u, w', w} J] {X : AlgebraicGeometry.Scheme} {K : CategoryTheory.Functor J X.Modules} (hK : ∀ (j : J), SheafOfModules.IsQuasicoherent (K.obj j)) {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) :
SheafOfModules.IsQuasicoherent c.pt

On any scheme, the colimit, in the category of all sheaves of modules, of a small diagram of quasicoherent sheaves is quasicoherent.

source
instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_isClosedUnderColimitsOfShape (J : Type w) [CategoryTheory.Category.{w', w} J] [CategoryTheory.EssentiallySmall.{u, w', w} J] (X : Scheme) :
(SheafOfModules.isQuasicoherent X.ringCatSheaf).IsClosedUnderColimitsOfShape J

Quasicoherence is closed under small colimits in the category of all sheaves of modules, so the generic full-subcategory construction supplies these colimits in QuasicoherentSheaf X.

source
instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.hasBinaryBiproducts (X : AlgebraicGeometry.Scheme) :
CategoryTheory.Limits.HasBinaryBiproducts (QuasicoherentSheaf X)

Quasicoherent sheaves are closed under binary coproducts in X.Modules, so the preadditive category QuasicoherentSheaf X has binary biproducts.

source
instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_sigma {X : Scheme} {ι : Type w} [Small.{u, w} ι] (M : ι → X.Modules) [CategoryTheory.Limits.HasCoproduct M] [∀ (i : ι), SheafOfModules.IsQuasicoherent (M i)] :
SheafOfModules.IsQuasicoherent (∐ M)

The coproduct of a small family of quasicoherent sheaves on any scheme is quasicoherent.

source
noncomputable def AlgebraicGeometry.IsAffineOpen.restrictFromSpecCompModuleSpecΓFunctorIso {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) :
(Scheme.Modules.restrictFunctor hU.fromSpec).comp moduleSpecΓFunctor ≅ Scheme.Modules.sectionsFunctor U

Over an affine open U, the sections functor is global sections on the affine chart Spec Γ(X, U) ⟶ X, naturally in the module: the components are fromSpecSectionsEquiv.

Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.IsAffineOpen.restrictFromSpecCompModuleSpecΓFunctorIso_hom_app {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (M : X.Modules) :
    hU.restrictFromSpecCompModuleSpecΓFunctorIso.hom.app M = ModuleCat.ofHom ↑(M.fromSpecSectionsEquiv hU).symm

    The components of restrictFromSpecCompModuleSpecΓFunctorIso are the inverses of fromSpecSectionsEquiv.

    source
    @[simp]
    theorem AlgebraicGeometry.IsAffineOpen.restrictFromSpecCompModuleSpecΓFunctorIso_inv_app {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (M : X.Modules) :
    hU.restrictFromSpecCompModuleSpecΓFunctorIso.inv.app M = ModuleCat.ofHom ↑(M.fromSpecSectionsEquiv hU)

    The components of the inverse of restrictFromSpecCompModuleSpecΓFunctorIso are fromSpecSectionsEquiv.

    source
    noncomputable def TauCeti.AlgebraicGeometry.isColimitMapCoconeSectionsFunctor {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.EssentiallySmall.{u, w', w} J] {X : AlgebraicGeometry.Scheme} {U : X.Opens} {K : CategoryTheory.Functor J X.Modules} (hK : ∀ (j : J), SheafOfModules.IsQuasicoherent (K.obj j)) {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (hU : AlgebraicGeometry.IsAffineOpen U) :
    CategoryTheory.Limits.IsColimit ((AlgebraicGeometry.Scheme.Modules.sectionsFunctor U).mapCocone c)

    Sections over an affine open send a colimit, in the category of all sheaves of modules, of a small diagram of quasicoherent sheaves to a colimit of Γ(X, U)-modules.

    Instances For
      source
      theorem TauCeti.AlgebraicGeometry.toModule_sectionsFunctor_map_bijective {ι : Type w} [DecidableEq ι] {X : AlgebraicGeometry.Scheme} {U : X.Opens} {M : ι → X.Modules} [∀ (i : ι), SheafOfModules.IsQuasicoherent (M i)] {P : X.Modules} {g : (i : ι) → M i ⟶ P} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)) (hU : AlgebraicGeometry.IsAffineOpen U) :
      Function.Bijective ⇑(DirectSum.toModule (↑(X.presheaf.obj (Opposite.op U))) ι ↑((AlgebraicGeometry.Scheme.Modules.sectionsFunctor U).obj P) fun (i : ι) => ModuleCat.Hom.hom ((AlgebraicGeometry.Scheme.Modules.sectionsFunctor U).map (g i)))

      If P is the coproduct of a family of quasicoherent sheaves Mᵢ, with coprojections gᵢ, then over an affine open U the induced map ⨁ᵢ Γ(Mᵢ, U) → Γ(P, U) is bijective. The scheme lives in a universe at least that of the index type, so that the direct sum is a module in the universe of the sections.