Bounded-below derived affine global sections #

The affine global-sections functor from module sheaves on Spec R to modules has a right derived functor on Mathlib's bounded-below derived category. Its unit carries Mathlib's right-derived universal property. The construction uses injective resolutions of all module sheaves, with no quasicoherence assumption on their terms or on the input. Finite-limit preservation of affine sections specializes the generic H⁰ unit theorem to all affine module sheaves, without a quasicoherence premise.

Main definitions #

This file introduces no carrier or category. The additive structure needed for the existing affine global-sections functor is local to this construction.

Main results #

AlgebraicGeometry.Cohomology.affineRGammaPlus is the bounded-below right derived global-sections functor.
AlgebraicGeometry.Cohomology.affineRGammaPlusUnit is its derived unit.
AlgebraicGeometry.Cohomology.affineRGammaPlusHomologyZeroSingleIso is the pointwise comparison on degree-zero single objects.
AlgebraicGeometry.Cohomology.affineRGammaPlusHomologyZeroSingleNatIso is the natural comparison on degree-zero single objects.
AlgebraicGeometry.Cohomology.affineRGammaPlus_isRightDerivedFunctor records the right-derived universal property.
AlgebraicGeometry.Cohomology.isIso_homologyZero_map_affineRGammaPlusUnit_of_isStrictlyGE_zero gives the H⁰ unit isomorphism on strictly nonnegative complexes.
AlgebraicGeometry.Cohomology.affineRGammaPlusHomologyZeroOfIsStrictlyGEZero identifies derived affine H⁰ with ordinary sections of input H⁰ for a strictly nonnegative complex.

Implementation notes #

Finite-product preservation makes the affine sections functor additive. Mathlib's CategoryTheory.Functor.rightDerivedFunctorPlus constructs the functor and its unit from that fact and enough injectives in the category of module sheaves. Finite-limit preservation discharges both outgoing-kernel premises of the generic H⁰ theorem. The degree-zero single comparison is natural and agrees with its pointwise predecessor. No natural H⁰ identification on arbitrary bounded-below Dqc objects follows.

References #

Mathlib's CategoryTheory.Functor.rightDerivedFunctorPlus and CategoryTheory.Functor.rightDerivedFunctorPlusUnit at the pinned revision; the affine source functor is AlgebraicGeometry.affineΓ.

Tags #

affine scheme, global sections, right derived functor, bounded below

source

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlus (R : CommRingCat) :

CategoryTheory.Functor (DerivedCategory.Plus (Spec R).Modules) (DerivedCategory.Plus (ModuleCat ↑R))

Right-derived global sections of module sheaves on an affine scheme, restricted to Mathlib's bounded-below derived categories. The definition itself uses no H⁰ comparison or unbounded Dqc identification.

Equations

AlgebraicGeometry.Cohomology.affineRGammaPlus R = (AlgebraicGeometry.affineΓ R).rightDerivedFunctorPlus

Instances For

source

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlusUnit (R : CommRingCat) :

(affineΓ R).mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh ⟶ DerivedCategory.Plus.Qh.comp (affineRGammaPlus R)

Mathlib's injective-resolution construction supplies this comparison from homotopy-level affine sections to the bounded-below derived functor.

Equations

AlgebraicGeometry.Cohomology.affineRGammaPlusUnit R = (AlgebraicGeometry.affineΓ R).rightDerivedFunctorPlusUnit

Instances For

source

instance AlgebraicGeometry.Cohomology.affineRGammaPlus_isRightDerivedFunctor (R : CommRingCat) :

(affineRGammaPlus R).IsRightDerivedFunctor (affineRGammaPlusUnit R) (HomotopyCategory.Plus.quasiIso (Spec R).Modules)

This universal property is inherited by unfolding the specialization to Mathlib's right-derived functor; no affine acyclicity theorem is needed here.

source

theorem AlgebraicGeometry.Cohomology.isIso_homologyZero_map_affineRGammaPlusUnit_of_isStrictlyGE_zero (R : CommRingCat) (K : CochainComplex.Plus (Spec R).Modules) [K.obj.IsStrictlyGE 0] :

CategoryTheory.IsIso ((DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0).map ((affineRGammaPlusUnit R).app ((HomotopyCategory.Plus.quotient (Spec R).Modules).obj K)))

Affine sections preserve finite limits, so they preserve both the input's degree-zero outgoing kernel and those in its nonnegative injective resolutions. The generic right-derived unit theorem then gives an H⁰ isomorphism.

source

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlusHomologyZeroOfIsStrictlyGEZero (R : CommRingCat) (K : CochainComplex.Plus (Spec R).Modules) [K.obj.IsStrictlyGE 0] :

(DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0).obj ((affineRGammaPlus R).obj (DerivedCategory.Plus.Q.obj K)) ≅ (affineΓ R).obj (HomologicalComplex.homology K.obj 0)

On a strictly nonnegative complex of affine module sheaves, degree-zero homology of bounded-below derived global sections is ordinary affine sections of the input's degree-zero homology sheaf. No quasicoherence assumption is needed here. This statement uses the chosen complex representative; it does not identify derived sections of every bounded-below Dqc object.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlusHomologyZeroSingleIso (R : CommRingCat) (M : (Spec R).Modules) :

(DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0).obj ((affineRGammaPlus R).obj ((DerivedCategory.Plus.singleFunctor (Spec R).Modules 0).obj M)) ≅ (affineΓ R).obj M

On an arbitrary affine module sheaf, invert H⁰ of the derived unit on its degree-zero single and normalize the source to ordinary affine sections. Its agreement with the natural comparison below is proved separately.

Equations