Cohomology on the image of an open immersion

Let f : Y ⟶ X be an open immersion of schemes and M a sheaf of modules on X. This file identifies the cohomology Hⁿ(f(Y), M) of the open subset f(Y) of X with the cohomology Hⁿ(Y, M|_Y) of the restriction of M along f.

Applied to the canonical open immersion Spec Γ(X, U) ⟶ X of an affine open U, it transports the acyclicity of quasi-coherent sheaves on the spectrum of a Noetherian ring (Hartshorne, Theorem III.3.5) to the affine opens of an arbitrary scheme: a quasi-coherent sheaf has no cohomology in positive degrees on an affine open U with Γ(X, U) Noetherian.

Main declarations

• AlgebraicGeometry.Scheme.Modules.cohomologyOnOpensRangeNatIso: the comparison Hⁿ(f(Y), M) ≅ Hⁿ(Y, M|_Y), natural in M, and cohomologyOnOpensRangeIso its component at a single sheaf of modules.
• AlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_succ_of_isAffineOpen: acyclicity of quasi-coherent sheaves on Noetherian affine opens.

References

• R. Hartshorne, Algebraic Geometry, Chapter III, Theorem 3.5 and Theorem 3.7.

noncomputable def AlgebraicGeometry.Scheme.Modules.overPullbackSheafCongrIsoRestrict {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] [CategoryTheory.Functor.IsDenseSubsite (Opens.grothendieckTopology ↥Y) ((Opens.grothendieckTopology ↥X).over (Hom.opensRange f)) ⋯.overEquivalence.inverse] : (SheafOfModules.toSheaf X.ringCatSheaf).comp (((Opens.grothendieckTopology ↥X).overPullback AddCommGrpCat (Hom.opensRange f)).comp (CategoryTheory.Equivalence.sheafCongr ((Opens.grothendieckTopology ↥X).over (Hom.opensRange f)) (Opens.grothendieckTopology ↥Y) ⋯.overEquivalence AddCommGrpCat).functor) ≅ (restrictFunctor f).comp (SheafOfModules.toSheaf Y.ringCatSheaf)

Transporting the underlying sheaf of a sheaf of modules restricted to f.opensRange along the open-embedding equivalence agrees with restriction of modules along f.

Equations

• AlgebraicGeometry.Scheme.Modules.overPullbackSheafCongrIsoRestrict f = (SheafOfModules.toSheaf X.ringCatSheaf).isoWhiskerLeft (⋯.overPullbackSheafCongrIso AddCommGrpCat)

noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyOnOpensRangeNatIso {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] (n : ℕ) : (SheafOfModules.toSheaf X.ringCatSheaf).comp ((CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↥X) n).comp ((CategoryTheory.evaluation X.Opensᵒᵖ AddCommGrpCat).obj (Opposite.op (Hom.opensRange f)))) ≅ (restrictFunctor f).comp (TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor Y n)

The cohomology of a sheaf of modules on the image of an open immersion f : Y ⟶ X is the cohomology of its restriction along f, naturally in the sheaf of modules.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyOnOpensRangeIso {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] (M : X.Modules) (n : ℕ) : TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOn M n (Hom.opensRange f) ≅ ↧(TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (M.restrict f) n)

The cohomology of a sheaf of modules M on the image of an open immersion f : Y ⟶ X is the cohomology of the restriction of M along f.

Equations

• AlgebraicGeometry.Scheme.Modules.cohomologyOnOpensRangeIso f M n = (AlgebraicGeometry.Scheme.Modules.cohomologyOnOpensRangeNatIso f n).app M

theorem AlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_succ_of_isAffineOpen {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] {U : X.Opens} (hU : IsAffineOpen U) [IsNoetherianRing ↑(X.presheaf.obj (Opposite.op U))] (n : ℕ) : Subsingleton ↑(TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOn M (n + 1) U)

Acyclicity of quasi-coherent sheaves on affine opens: a quasi-coherent sheaf of modules has no cohomology in positive degrees on an affine open subset U whose ring of sections is Noetherian.