Exact pushforward along a closed embedding

Pushforward of abelian sheaves along a closed embedding is exact. At a point of the image its stalk is the original stalk, and outside the closed image its stalk is zero. This is the exactness input for comparing sheaf cohomology with cohomology on a closed subspace, for example when embedding a projective scheme in projective space.

References

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

instance TauCeti.Topology.additive_pushforward {X Y : TopCat} (f : X ⟶ Y) : (TopCat.Sheaf.pushforward AddCommGrpCat f).Additive

Direct image of abelian sheaves is additive.

theorem TauCeti.Topology.isZero_stalk_pushforward_of_notMem_closure_range {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Sheaf AddCommGrpCat X) {y : ↑Y} (hy : y ∉ closure (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))) : CategoryTheory.Limits.IsZero (TopCat.Presheaf.stalk ((TopCat.Sheaf.pushforward AddCommGrpCat f).obj F).obj y)

The stalk of a pushed-forward abelian sheaf vanishes outside the closure of the image.

noncomputable def TauCeti.Topology.pushforwardStalkIso {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : (TopCat.Sheaf.pushforward AddCommGrpCat f).comp ((TopCat.Sheaf.forget AddCommGrpCat Y).comp (TopCat.Presheaf.stalkFunctor AddCommGrpCat ((CategoryTheory.ConcreteCategory.hom f) x))) ≅ (TopCat.Sheaf.forget AddCommGrpCat X).comp (TopCat.Presheaf.stalkFunctor AddCommGrpCat x)

For an inducing map, the stalk of pushforward at an image point is naturally isomorphic to the original stalk.

@[simp]

theorem TauCeti.Topology.pushforwardStalkIso_hom_app {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) (F : TopCat.Sheaf AddCommGrpCat X) : (pushforwardStalkIso f hf x).hom.app F = TopCat.Presheaf.stalkPushforward AddCommGrpCat f F.obj x

The stalk comparison is the canonical pushforward map on stalks.

theorem TauCeti.Topology.exact_pushforward_of_isClosedEmbedding {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)) (hS : S.Exact) : (S.map (TopCat.Sheaf.pushforward AddCommGrpCat f)).Exact

Pushforward along a closed embedding preserves exact complexes of abelian sheaves.

theorem TauCeti.Topology.preservesHomology_pushforward_of_isClosedEmbedding {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (TopCat.Sheaf.pushforward AddCommGrpCat f).PreservesHomology

Closed-embedding pushforward preserves homology.

theorem TauCeti.Topology.preservesFiniteColimits_pushforward_of_isClosedEmbedding {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Limits.PreservesFiniteColimits (TopCat.Sheaf.pushforward AddCommGrpCat f)

Closed-embedding pushforward preserves finite colimits, as well as the limits preserved by every sheaf pushforward.