Kernels of quasicoherent sheaves

The kernel, in the category of all sheaves of modules on a scheme, of a morphism between quasicoherent sheaves is quasicoherent. No finiteness, separation, or Noetherian hypothesis is needed. Consequently the full subcategory of quasicoherent sheaves has kernels, and its inclusion creates them. This allows kernel presentations of sheaf internal Hom to be used inside quasicoherent sheaves. Restriction to an open subscheme preserves the resulting kernels; its comparison is Mathlib's CategoryTheory.Limits.PreservesKernel.iso.

The affine calculation uses the exactness of AlgebraicGeometry.tilde.functor and Mathlib's tilde.adjunction. Restriction to affine opens then gives the result on arbitrary schemes.

References

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

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

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

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_isClosedUnderKernels (X : Scheme) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsClosedUnderKernels

Quasicoherence is closed under ambient kernels. The generic full-subcategory construction therefore supplies kernels in QuasicoherentSheaf X.

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

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