Evaluation into bounded-below derived affine sections

The single-object H⁰ comparison sends the identity of the structure sheaf to a class in derived affine sections. Applying derived sections and H⁰ to a map out of the structure sheaf, then evaluating at that class, gives an additive and target-natural map on arbitrary bounded-below derived objects.

The map is not asserted bijective here. In particular, this file does not identify H⁰ of derived sections of an arbitrary Dqc object with ordinary sections of its degree-zero cohomology sheaf.

Main definitions

• affineRGammaPlusUnitClass is the image of the structure-sheaf identity.
• affineRGammaPlusEval and affineRGammaPlusEvalAddHom are the specific evaluation map, as a function and additive homomorphism.

Main results

affineRGammaPlusEval_naturality gives target naturality.

Implementation notes

The existing single-object H⁰ comparison constructs the distinguished class. Generic additivity of bounded-below right-derived functors makes evaluation additive. No injective model or inverse is chosen in this file.

References

affineRGammaPlusHomologyZeroSingleIso and Scheme.Modules.unitHomTopLinearEquiv in this repository; Mathlib RightDerivedFunctorPlus.lean at pin 520045ab14e26149ee970e2e617ca04b09bde5d6.

Tags

affine scheme, derived global sections, evaluation, bounded below

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlusUnitClass (R : CommRingCat) : ↑((DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0).obj ((affineRGammaPlus R).obj ((DerivedCategory.Plus.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)))))

The class of the identity of the structure sheaf, transported through the existing H⁰ comparison on a degree-zero single object.

Equations

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

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlusEval (R : CommRingCat) (M : DerivedCategory.Plus (Spec R).Modules) (f : (DerivedCategory.Plus.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)) ⟶ M) : ↑((DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0).obj ((affineRGammaPlus R).obj M))

Apply bounded-below derived affine sections to a map out of the structure sheaf and evaluate its H⁰ map at affineRGammaPlusUnitClass. This is the specific map whose injective-model comparison remains to be proved; no inverse is claimed.

Equations

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

theorem AlgebraicGeometry.Cohomology.affineRGammaPlusEval_naturality (R : CommRingCat) {M N : DerivedCategory.Plus (Spec R).Modules} (f : (DerivedCategory.Plus.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)) ⟶ M) (g : M ⟶ N) : affineRGammaPlusEval R N (CategoryTheory.CategoryStruct.comp f g) = (ModuleCat.Hom.hom (((affineRGammaPlus R).comp (DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0)).map g)) (affineRGammaPlusEval R M f)

Naturality in the bounded-below target follows from functoriality of derived affine sections.

noncomputable def AlgebraicGeometry.Cohomology.affineRGammaPlusEvalAddHom (R : CommRingCat) (M : DerivedCategory.Plus (Spec R).Modules) : ((DerivedCategory.Plus.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)) ⟶ M) →+ ↑((DerivedCategory.Plus.homologyFunctor (ModuleCat ↑R) 0).obj ((affineRGammaPlus R).obj M))

The canonical evaluation map is additive. Additivity of bounded-below derived affine sections follows from the generic injective-model theorem; it is not supplied as an extra hypothesis.

Equations

• AlgebraicGeometry.Cohomology.affineRGammaPlusEvalAddHom R M = { toFun := AlgebraicGeometry.Cohomology.affineRGammaPlusEval R M, map_zero' := ⋯, map_add' := ⋯ }