Cohomology of a coherent sheaf along a closed immersion

cohCohomologyPushforwardAddEquiv : Hⁿ(X, F) ≃+ Hⁿ(Y, ι_* F) for ι a closed immersion of schemes and F coherent on X, with ι_* F itself coherent. This closes the last gap between CohomologyPushforward.lean's abelian-sheaf statement and #572 step 3's acceptance criterion, which is phrased for coherent sheaves.

The passage from modules to abelian sheaves is rfl

toSheaf_pushforward records that Scheme.Modules.toSheaf commutes with pushforward on the nose: the module pushforward is the abelian pushforward carrying a module structure, so the two composites are the same abelian sheaf.

This is worth stating because the shape — a functor commuting with a functor — looks like it needs a comparison isomorphism and does not. It is the last of several places on this lane where an unchecked definitional fact was mistaken for unbuilt mathematics; the others were the site bridge (also rfl) and the EnoughInjectives/HasExt instances (imports).

What makes the target coherent

Scheme.isCoherent_pushforward, #572 step 2. cohPushforward packages the module pushforward of a coherent sheaf with that proof, as an object of Coh Y. IsLocallyNoetherian Y is spent entirely there — the cohomology comparison needs no chain condition of its own.

One way this is still weaker than #572's wording

The HasExt universe is pinned, because the instantiation lets instance search find it. Topology/Sheaves/CohomologyPushforward.lean keeps it positional (cohomologyPushforwardAddEquivAt) for callers who need another witness; the coherent-cohomology convention HasExt.standard is one such caller, in Cohomology/Finiteness/ProjectiveVariety.lean, where the comparison is also shown natural in F and k-linear.

Main results

• toSheaf_pushforward — the passage, by rfl.
• cohPushforward — ι_* F as a coherent sheaf.
• modulesCohomologyPushforwardAddEquiv, cohCohomologyPushforwardAddEquiv — the comparison.

theorem AlgebraicGeometry.Scheme.toSheaf_pushforward {X Y : Scheme} (g : X ⟶ Y) (F : X.Modules) : (Modules.toSheaf Y).obj ((Modules.pushforward g).obj F) = ((TopologicalSpace.Opens.map g.base).sheafPushforwardContinuous AddCommGrpCat (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X)).obj ((Modules.toSheaf X).obj F)

toSheaf commutes with pushforward, on the nose.

No hypothesis on g at all: this holds for any morphism of schemes.

noncomputable def AlgebraicGeometry.Scheme.modulesCohomologyPushforwardAddEquiv {X Y : Scheme} (g : X ⟶ Y) [IsClosedImmersion g] (F : X.Modules) (n : ℕ) : ((Modules.toSheaf X).obj F).H n ≃+ ((Modules.toSheaf Y).obj ((Modules.pushforward g).obj F)).H n

Cohomology of a module sheaf is unchanged by pushforward along a closed immersion.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.cohPushforward {X Y : Scheme} (g : X ⟶ Y) [IsClosedImmersion g] [IsLocallyNoetherian Y] (F : Coh X) : Coh Y

ι_* F as a coherent sheaf, by #572 step 2.

Equations

• AlgebraicGeometry.Scheme.cohPushforward g F = { obj := (AlgebraicGeometry.Scheme.Modules.pushforward g).obj ((AlgebraicGeometry.Coh.ι X).obj F), property := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.cohCohomologyPushforwardAddEquiv {X Y : Scheme} (g : X ⟶ Y) [IsClosedImmersion g] [IsLocallyNoetherian Y] (F : Coh X) (n : ℕ) : ((Modules.toSheaf X).obj ((Coh.ι X).obj F)).H n ≃+ ((Modules.toSheaf Y).obj ((Coh.ι Y).obj (cohPushforward g F))).H n

#572 step 3 for coherent sheaves.

Equations

• AlgebraicGeometry.Scheme.cohCohomologyPushforwardAddEquiv g F n = AlgebraicGeometry.Scheme.modulesCohomologyPushforwardAddEquiv g ((AlgebraicGeometry.Coh.ι X).obj F) n