Cohomology and pushforward along a closed immersion #
This algebraic-geometry leaf specializes the space-level comparison from
Topology/Sheaves/CohomologyPushforward.lean to the underlying map of a closed
immersion of schemes. Keeping the specialization here prevents the generic CategoryTheory layer
from importing algebraic geometry.
noncomputable def
DerivedAlgGeo.AlgebraicGeometry.schemeCohomologyPushforwardAddEquiv
{X Y : AlgebraicGeometry.Scheme}
(g : X ⟶ Y)
[AlgebraicGeometry.IsClosedImmersion g]
(F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥X) AddCommGrpCat)
(n : ℕ)
:
F.H n ≃+ (((TopologicalSpace.Opens.map g.base).sheafPushforwardContinuous AddCommGrpCat (Opens.grothendieckTopology ↥Y)
(Opens.grothendieckTopology ↥X)).obj
F).H
n
#572 step 3 at a closed immersion of schemes.
Hⁿ(X, F) ≃+ Hⁿ(Y, ι_* F). A closed immersion is a closed embedding on underlying spaces
(IsClosedImmersion.isClosedEmbedding), which supplies both hypotheses of the topological
statement directly.
This is an isomorphism for each abelian sheaf F; naturality in F, a universe-parametric
HasExt, and the passage from coherent sheaves to abelian sheaves remain separate work.