Cohomology of pushforward from a closed subspace

For a closed embedding f : X ⟶ Y, the cohomology of f_* F over an open U of Y is naturally isomorphic to the cohomology of F over f⁻¹(U). The comparison uses Mathlib's CategoryTheory.Adjunction.extEquiv for the exact inverse-image/direct-image adjunction, and identifies the first Ext argument by the comparison CategoryTheory.Functor.freeYonedaSheafToSheafPullback of free abelian sheaves.

References

• R. Hartshorne, Algebraic Geometry, III, Lemma 2.10.

noncomputable def TauCeti.Topology.pullbackFreeYonedaIso {X Y : TopCat} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y) : (TopCat.Sheaf.pullback AddCommGrpCat f).obj ((CategoryTheory.freeYonedaSheafFunctor (Opens.grothendieckTopology ↑Y)).obj U) ≅ (CategoryTheory.freeYonedaSheafFunctor (Opens.grothendieckTopology ↑X)).obj ((TopologicalSpace.Opens.map f).obj U)

Inverse image takes the free abelian sheaf on U to the free abelian sheaf on f⁻¹(U): the inverse of the comparison CategoryTheory.Functor.freeYonedaSheafToSheafPullback for Opens.map f.

noncomputable def TauCeti.Topology.cohomologyPushforwardNatIso {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (n : ℕ) (U : TopologicalSpace.Opens ↑Y) : (TopCat.Sheaf.pushforward AddCommGrpCat f).comp ((CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↑Y) n).comp ((CategoryTheory.evaluation (TopologicalSpace.Opens ↑Y)ᵒᵖ AddCommGrpCat).obj (Opposite.op U))) ≅ (CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↑X) n).comp ((CategoryTheory.evaluation (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat).obj (Opposite.op ((TopologicalSpace.Opens.map f).obj U)))

Cohomology over U of the direct image from a closed subspace is cohomology over f⁻¹(U), naturally in the coefficient sheaf.

noncomputable def TauCeti.Topology.cohomologyPushforwardIso {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (F : TopCat.Sheaf AddCommGrpCat X) (n : ℕ) (U : TopologicalSpace.Opens ↑Y) : CategoryTheory.Sheaf.H' ((TopCat.Sheaf.pushforward AddCommGrpCat f).obj F) n U ≅ CategoryTheory.Sheaf.H' F n ((TopologicalSpace.Opens.map f).obj U)

The cohomology of a pushed-forward abelian sheaf along a closed embedding agrees with the original cohomology over the inverse-image open.

@[simp]

theorem TauCeti.Topology.cohomologyPushforwardNatIso_app {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (F : TopCat.Sheaf AddCommGrpCat X) (n : ℕ) (U : TopologicalSpace.Opens ↑Y) : (cohomologyPushforwardNatIso f hf n U).app F = cohomologyPushforwardIso f hf F n U

The coefficientwise comparison is the component of the natural comparison.

@[simp]

theorem TauCeti.Topology.cohomologyPushforwardNatIso_hom_app {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (F : TopCat.Sheaf AddCommGrpCat X) (n : ℕ) (U : TopologicalSpace.Opens ↑Y) : (cohomologyPushforwardNatIso f hf n U).hom.app F = (cohomologyPushforwardIso f hf F n U).hom

theorem TauCeti.Topology.cohomologyPushforwardIso_naturality {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {F G : TopCat.Sheaf AddCommGrpCat X} (α : F ⟶ G) (n : ℕ) (U : TopologicalSpace.Opens ↑Y) : CategoryTheory.CategoryStruct.comp (((TopCat.Sheaf.pushforward AddCommGrpCat f).comp ((CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↑Y) n).comp ((CategoryTheory.evaluation (TopologicalSpace.Opens ↑Y)ᵒᵖ AddCommGrpCat).obj (Opposite.op U)))).map α) (cohomologyPushforwardIso f hf G n U).hom = CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIso f hf F n U).hom (((CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↑X) n).comp ((CategoryTheory.evaluation (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat).obj (Opposite.op ((TopologicalSpace.Opens.map f).obj U)))).map α)

The cohomology comparison commutes with maps of coefficient sheaves.

theorem TauCeti.Topology.cohomologyPushforwardIso_naturality_assoc {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {F G : TopCat.Sheaf AddCommGrpCat X} (α : F ⟶ G) (n : ℕ) (U : TopologicalSpace.Opens ↑Y) {Z : AddCommGrpCat} (h : CategoryTheory.Sheaf.H' G n ((TopologicalSpace.Opens.map f).obj U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.evaluation (TopologicalSpace.Opens ↑Y)ᵒᵖ AddCommGrpCat).obj (Opposite.op U)).map ((CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↑Y) n).map ((TopCat.Sheaf.pushforward AddCommGrpCat f).map α))) (CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIso f hf G n U).hom h) = CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIso f hf F n U).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.evaluation (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat).obj (Opposite.op ((TopologicalSpace.Opens.map f).obj U))).map ((CategoryTheory.Sheaf.cohomologyPresheafFunctor (Opens.grothendieckTopology ↑X) n).map α)) h)

The cohomology comparison commutes with maps of coefficient sheaves.