Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Abelian.Kernels

Kernels and cokernels of coherent sheaves #

On a locally noetherian scheme, coherent module sheaves are closed under kernels and cokernels in the ambient category of module sheaves.

For kernels, the substantive affine input is that localization commutes with kernels. Applied to restriction from Spec R to every basic open, this identifies the ambient kernel with the tilde sheaf of its global sections. The global sections form a finite module because they are a submodule of the finite global sections of the source over a noetherian ring.

For cokernels, tilde is a left adjoint and therefore preserves cokernels. The affine comparison counits identify the ambient cokernel with the tilde sheaf of the cokernel on global sections, which is finite as a quotient of the finite global sections of the target.

The affine-local criterion then globalizes both results. The final object-property instances give Coh X kernels and cokernels through Mathlib's full-subcategory infrastructure.

Main results #

source
instance AlgebraicGeometry.modulesSpecToSheaf_preservesFiniteLimits (R : CommRingCat) :
CategoryTheory.Limits.PreservesFiniteLimits modulesSpecToSheaf

The forgetful functor from module sheaves on Spec R to sheaves of R-modules preserves finite limits.

source
instance AlgebraicGeometry.Scheme.Modules.restrictFunctor_preservesFiniteLimits {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :
CategoryTheory.Limits.PreservesFiniteLimits (restrictFunctor f)

Scheme-level restriction along an open immersion preserves finite limits.

source
noncomputable def AlgebraicGeometry.moduleSpecSectionsFunctor (R : CommRingCat) (U : (Spec R).Opens) :
CategoryTheory.Functor (Spec R).Modules (ModuleCat ↑R)

Sections of an 𝒪_{Spec R}-module over an open, as a functor to R-modules.

This is Mathlib's moduleSpecΓFunctor for a general open — and, at U = ⊤, retyped. The retyping is the point: moduleSpecΓFunctor has domain (Spec (.of R)).Modules, which is defeq to (Spec R).Modules but not to instance search, so an instance proved for one is not found for the other. Everything downstream states its geometry over (Spec R).Modules, so it wants this one. Modules/Affine/Equivalence.lean records the same wrapper problem for Scheme.Modules itself.

Public rather than private since #720: the quasi-coherent extension argument needs ShortComplex.map through it, which means the instances below have to be reachable from another file.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance AlgebraicGeometry.moduleSpecSectionsFunctor_preservesFiniteLimits {R : CommRingCat} (U : (Spec R).Opens) :
    CategoryTheory.Limits.PreservesFiniteLimits (moduleSpecSectionsFunctor R U)

    Sections over an open preserve finite limits.

    source
    instance AlgebraicGeometry.moduleSpecSectionsFunctor_preservesZeroMorphisms {R : CommRingCat} (U : (Spec R).Opens) :
    (moduleSpecSectionsFunctor R U).PreservesZeroMorphisms

    Sections over an open preserve zero morphisms.

    source
    theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_kernel {R : CommRingCat} {M N : (Spec R).Modules} (g : M ⟶ N) (f : ↑R) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] :
    IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom ((CategoryTheory.Limits.kernel g).basicOpenRestriction f))

    Restriction to a basic open is a localization for the kernel of a morphism between quasi-coherent module sheaves.

    source
    theorem AlgebraicGeometry.Scheme.Modules.isCoherent_kernel_affine {R : CommRingCat} [IsNoetherianRing ↑R] {M N : (Spec R).Modules} (g : M ⟶ N) (hM : IsCoherent (Spec R) M) (hN : IsCoherent (Spec R) N) :
    IsCoherent (Spec R) (CategoryTheory.Limits.kernel g)

    Kernels of morphisms between coherent module sheaves on an affine noetherian scheme are coherent.

    source
    theorem AlgebraicGeometry.Scheme.Modules.isCoherent_cokernel_affine {R : CommRingCat} [IsNoetherianRing ↑R] {M N : (Spec R).Modules} (g : M ⟶ N) (hM : IsCoherent (Spec R) M) (hN : IsCoherent (Spec R) N) :
    IsCoherent (Spec R) (CategoryTheory.Limits.cokernel g)

    Cokernels of morphisms between coherent module sheaves on an affine noetherian scheme are coherent.

    source
    noncomputable def AlgebraicGeometry.Scheme.Modules.restrictKernelIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {M N : Y.Modules} (g : M ⟶ N) :
    (CategoryTheory.Limits.kernel g).restrict f ≅ CategoryTheory.Limits.kernel ((restrictFunctor f).map g)

    Restriction along an open immersion commutes with kernels.

    Equations
    Instances For
      source
      noncomputable def AlgebraicGeometry.Scheme.Modules.restrictCokernelIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {M N : Y.Modules} (g : M ⟶ N) :
      (CategoryTheory.Limits.cokernel g).restrict f ≅ CategoryTheory.Limits.cokernel ((restrictFunctor f).map g)

      Restriction along an open immersion commutes with cokernels.

      Equations
      Instances For
        source
        theorem AlgebraicGeometry.Scheme.Modules.isCoherent_kernel {X : Scheme} [IsLocallyNoetherian X] {M N : X.Modules} (g : M ⟶ N) (hM : IsCoherent X M) (hN : IsCoherent X N) :
        IsCoherent X (CategoryTheory.Limits.kernel g)

        Kernels of morphisms between coherent module sheaves on a locally noetherian scheme are coherent.

        source
        theorem AlgebraicGeometry.Scheme.Modules.isCoherent_cokernel {X : Scheme} [IsLocallyNoetherian X] {M N : X.Modules} (g : M ⟶ N) (hM : IsCoherent X M) (hN : IsCoherent X N) :
        IsCoherent X (CategoryTheory.Limits.cokernel g)

        Cokernels of morphisms between coherent module sheaves on a locally noetherian scheme are coherent.

        source
        instance AlgebraicGeometry.Scheme.coherent_isClosedUnderKernels {X : Scheme} [IsLocallyNoetherian X] :
        X.coherent.IsClosedUnderKernels

        Coherent module sheaves on a locally noetherian scheme are closed under kernels in the ambient module-sheaf category.

        source
        instance AlgebraicGeometry.Scheme.coherent_isClosedUnderCokernels {X : Scheme} [IsLocallyNoetherian X] :
        X.coherent.IsClosedUnderCokernels

        Coherent module sheaves on a locally noetherian scheme are closed under cokernels in the ambient module-sheaf category.