Documentation

TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.Affine

Coherent sheaves on the spectrum of a Noetherian ring #

For a Noetherian ring R, finitely presented sheaves on Spec R are precisely the sheaves associated with finite R-modules. Restricting the tilde/global-sections adjunction gives an equivalence with FGModuleCat R. In particular, this category of coherent sheaves is abelian, and its inclusion into all sheaves of modules is exact.

The kernel and cokernel of a morphism of coherent sheaves, computed in all module sheaves, are again coherent. Thus short exact sequences of coherent sheaves can be used in sheaf cohomology without changing their ambient kernels or cokernels. The cokernel result needs no Noetherian hypothesis; the kernel result does.

The construction follows Mathlib's AlgebraicGeometry.tildeEquiv and uses the finite-presentation comparison for tilde sheaves, rather than a new definition of coherence.

References #

source
noncomputable def TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeFunctor (R : CommRingCat) [IsNoetherianRing ↑R] :
CategoryTheory.Functor (FGModuleCat ↑R) (FinitelyPresentedSheaf (AlgebraicGeometry.Spec R))

Associate a coherent sheaf on Spec R to a finite module over the Noetherian ring R.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.globalSectionsFunctor (R : CommRingCat) :
    CategoryTheory.Functor (FinitelyPresentedSheaf (AlgebraicGeometry.Spec R)) (FGModuleCat ↑R)

    Global sections of a finitely presented sheaf on Spec R, as a finite R-module.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeFunctor_comp_inclusion (R : CommRingCat) [IsNoetherianRing ↑R] :
      (tildeFunctor R).comp (SheafOfModules.isFinitePresentation (AlgebraicGeometry.Spec R).ringCatSheaf).ι = (CategoryTheory.forget₂ (FGModuleCat ↑R) (ModuleCat ↑R)).comp (AlgebraicGeometry.tilde.functor R)

      After forgetting finite presentation, this is the usual associated-sheaf functor.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.globalSectionsFunctor_comp_forget (R : CommRingCat) :
      (globalSectionsFunctor R).comp (CategoryTheory.forget₂ (FGModuleCat ↑R) (ModuleCat ↑R)) = (SheafOfModules.isFinitePresentation (AlgebraicGeometry.Spec R).ringCatSheaf).ι.comp AlgebraicGeometry.moduleSpecΓFunctor

      After forgetting finiteness, this is the usual global-section functor.

      source
      noncomputable def TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv (R : CommRingCat) [IsNoetherianRing ↑R] :
      FGModuleCat ↑R ≌ FinitelyPresentedSheaf (AlgebraicGeometry.Spec R)

      Coherent sheaves on Spec R are equivalent to finite R-modules. The functors are tilde and global sections, with the unit and counit inherited from the tilde adjunction.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv_functor (R : CommRingCat) [IsNoetherianRing ↑R] :
        (tildeEquiv R).functor = tildeFunctor R

        The forward equivalence functor associates a sheaf to a finite module.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv_inverse (R : CommRingCat) [IsNoetherianRing ↑R] :
        (tildeEquiv R).inverse = globalSectionsFunctor R

        The inverse equivalence functor takes global sections.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv_unitIso_hom_app_hom (R : CommRingCat) [IsNoetherianRing ↑R] (M : FGModuleCat ↑R) :
        ((tildeEquiv R).unitIso.hom.app M).hom = AlgebraicGeometry.tilde.toTildeΓNatIso.hom.app M.obj

        The underlying unit component is the unit of the tilde adjunction.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv_unitIso_inv_app_hom (R : CommRingCat) [IsNoetherianRing ↑R] (M : FGModuleCat ↑R) :
        ((tildeEquiv R).unitIso.inv.app M).hom = AlgebraicGeometry.tilde.toTildeΓNatIso.inv.app M.obj

        The underlying inverse unit component is the inverse of the tilde unit.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv_counitIso_hom_app_hom (R : CommRingCat) [IsNoetherianRing ↑R] (M : FinitelyPresentedSheaf (AlgebraicGeometry.Spec R)) :
        ((tildeEquiv R).counitIso.hom.app M).hom = AlgebraicGeometry.Scheme.Modules.fromTildeΓ M.obj

        The underlying counit component is the canonical map from the tilde of global sections.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.tildeEquiv_counitIso_inv_app_hom (R : CommRingCat) [IsNoetherianRing ↑R] (M : FinitelyPresentedSheaf (AlgebraicGeometry.Spec R)) :
        ((tildeEquiv R).counitIso.inv.app M).hom = (CategoryTheory.asIso (AlgebraicGeometry.Scheme.Modules.fromTildeΓ M.obj)).inv

        The underlying inverse counit component is the inverse of the canonical tilde map.

        source
        @[instance_reducible]
        noncomputable instance TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.instAbelianSpec (R : CommRingCat) [IsNoetherianRing ↑R] :
        CategoryTheory.Abelian (FinitelyPresentedSheaf (AlgebraicGeometry.Spec R))

        Coherent sheaves on the spectrum of a Noetherian ring form an abelian category.

        Equations
        source
        instance TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.instAdditiveFGModuleCatCarrierSpecTildeFunctor (R : CommRingCat) [IsNoetherianRing ↑R] :
        (tildeFunctor R).Additive

        Associating a sheaf to a finite module is an additive functor.

        source
        instance TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.instAdditiveSpecFGModuleCatCarrierGlobalSectionsFunctor (R : CommRingCat) :
        (globalSectionsFunctor R).Additive

        Taking global sections of a finitely presented sheaf is additive.

        source
        instance TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.preservesFiniteLimits_inclusion (R : CommRingCat) [IsNoetherianRing ↑R] :
        CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.isFinitePresentation (AlgebraicGeometry.Spec R).ringCatSheaf).ι

        The inclusion of coherent sheaves into all module sheaves preserves finite limits.

        source
        instance TauCeti.AlgebraicGeometry.FinitelyPresentedSheaf.preservesFiniteColimits_inclusion (R : CommRingCat) [IsNoetherianRing ↑R] :
        CategoryTheory.Limits.PreservesFiniteColimits (SheafOfModules.isFinitePresentation (AlgebraicGeometry.Spec R).ringCatSheaf).ι

        The inclusion of coherent sheaves into all module sheaves preserves finite colimits.