Cokernels of quasicoherent sheaves

The cokernel in the category of all sheaves of modules of a morphism between quasicoherent sheaves is quasicoherent. On a spectrum it is the sheaf associated with the cokernel of the map on global sections. Restriction to affine opens gives the result on arbitrary schemes, without Noetherian or separation assumptions.

Consequently quasicoherent sheaves have cokernels and their inclusion preserves them.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.7.

noncomputable def AlgebraicGeometry.Scheme.Modules.tildeCokernelIso {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : tilde (CategoryTheory.Limits.cokernel (moduleSpecΓFunctor.map f)) ≅ CategoryTheory.Limits.cokernel f

The ambient cokernel of a morphism of quasicoherent sheaves on a spectrum is the sheaf associated with the cokernel of its map on global sections.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_π_comp_tildeCokernelIso_hom {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : CategoryTheory.CategoryStruct.comp (tilde.map (CategoryTheory.Limits.cokernel.π (moduleSpecΓFunctor.map f))) (tildeCokernelIso f).hom = CategoryTheory.CategoryStruct.comp N.fromTildeΓ (CategoryTheory.Limits.cokernel.π f)

The affine cokernel comparison intertwines the quotient maps through the counit of the associated-sheaf/global-sections adjunction.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_π_comp_tildeCokernelIso_hom_assoc {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] {Z : (Spec R).Modules} (h : CategoryTheory.Limits.cokernel f ⟶ Z) : CategoryTheory.CategoryStruct.comp (tilde.map (CategoryTheory.Limits.cokernel.π (moduleSpecΓFunctor.map f))) (CategoryTheory.CategoryStruct.comp (tildeCokernelIso f).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp N.fromTildeΓ (CategoryTheory.Limits.cokernel.π f)) h

The affine cokernel comparison intertwines the quotient maps through the counit of the associated-sheaf/global-sections adjunction.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_cokernel {X : Scheme} {M N : X.Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.cokernel f)

The ambient cokernel of a morphism of quasicoherent sheaves on any scheme is quasicoherent.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_isClosedUnderCokernels (X : Scheme) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsClosedUnderCokernels

Quasicoherence is closed under ambient cokernels, so the generic full-subcategory construction supplies cokernels in QuasicoherentSheaf X.

instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.inclusion_preservesCokernel {X : AlgebraicGeometry.Scheme} {E F : QuasicoherentSheaf X} (f : E ⟶ F) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι

The inclusion of quasicoherent sheaves preserves cokernels: their universal property is the one in the ambient category of all module sheaves.