Inverse image on the cohomology of abelian sheaves

Let f : X ⟶ Y be a continuous map and F a sheaf of abelian groups on Y. The inverse image functor f⁻¹ from abelian sheaves on Y to abelian sheaves on X is exact, and it carries the constant sheaf ℤ on Y to the constant sheaf ℤ on X (TopCat.Hom.pullbackConstantSheafIso, in TauCeti.Topology.Sheaves.Functors). Since Hⁿ(Y, F) is Extⁿ(ℤ, F) (Mathlib's CategoryTheory.Sheaf.H), applying f⁻¹ to extensions gives the canonical map

f.cohomologyPullback F n : Hⁿ(Y, F) →+ Hⁿ(X, f⁻¹ F).

It is natural in F, commutes with the connecting maps of short exact sequences, and in degree zero it is the map on global sections given by the unit F ⟶ f_* f⁻¹ F of the adjunction. These three properties make it a morphism of cohomological δ-functors. Composed with a comparison map f⁻¹ F ⟶ G, it gives the pullback maps on the cohomology of sheaves of modules on schemes.

Main declarations

• TopCat.Hom.cohomologyPullback: the map Hⁿ(Y, F) →+ Hⁿ(X, f⁻¹ F);
• TopCat.Hom.cohomologyPullback_map: its naturality in F;
• TopCat.Hom.cohomologyPullback_δ: its compatibility with connecting maps;
• TopCat.Hom.cohomologyPullback_zero: its description in degree zero.

References

• R. Hartshorne, Algebraic Geometry, Section III.1 (universal δ-functors) and Exercise III.8.1.

noncomputable def TopCat.Hom.cohomologyPullback {X Y : TopCat} (f : X ⟶ Y) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat) (n : ℕ) : F.H n →+ (((TopologicalSpace.Opens.map f).sheafPullback AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).obj F).H n

The inverse image map Hⁿ(Y, F) →+ Hⁿ(X, f⁻¹ F) on sheaf cohomology along a continuous map f : X ⟶ Y: the exact functor f⁻¹ applied to Extⁿ(ℤ, F), followed by the identification f⁻¹ ℤ ≅ ℤ of pullbackConstantSheafIso.

theorem TopCat.Hom.cohomologyPullback_apply {X Y : TopCat} (f : X ⟶ Y) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat) {n : ℕ} (x : F.H n) : (cohomologyPullback f F n) x = (CategoryTheory.Abelian.Ext.mk₀ (pullbackConstantSheafIso f ↧(ULift.{u, 0} ℤ)).inv).comp (CategoryTheory.Abelian.Ext.mapExactFunctor ((TopologicalSpace.Opens.map f).sheafPullback AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)) x) ⋯

The defining formula of cohomologyPullback.

theorem TopCat.Hom.cohomologyPullback_map {X Y : TopCat} (f : X ⟶ Y) {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat} (α : F ⟶ G) {n : ℕ} (x : F.H n) : (cohomologyPullback f G n) ((CategoryTheory.Sheaf.H.map α n) x) = (CategoryTheory.Sheaf.H.map (((TopologicalSpace.Opens.map f).sheafPullback AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).map α) n) ((cohomologyPullback f F n) x)

The inverse image map on cohomology is natural in the coefficient sheaf.

theorem TopCat.Hom.cohomologyPullback_δ {X Y : TopCat} (f : X ⟶ Y) {S : CategoryTheory.ShortComplex (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat)} (hS : S.ShortExact) {n₀ n₁ : ℕ} (h : n₀ + 1 = n₁) (x : S.X₃.H n₀) : (cohomologyPullback f S.X₁ n₁) ((CategoryTheory.Sheaf.H.δ hS n₀ n₁ h) x) = (CategoryTheory.Sheaf.H.δ ⋯ n₀ n₁ h) ((cohomologyPullback f S.X₃ n₀) x)

The inverse image map on cohomology commutes with the connecting maps of a short exact sequence of sheaves and of its (exact) inverse image.

theorem TopCat.Hom.cohomologyPullback_zero {X Y : TopCat} (f : X ⟶ Y) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat) (x : F.H 0) : (CategoryTheory.Sheaf.H.equiv₀ (((TopologicalSpace.Opens.map f).sheafPullback AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).obj F) CategoryTheory.Limits.isTerminalTop) ((cohomologyPullback f F 0) x) = (CategoryTheory.ConcreteCategory.hom ((((TopologicalSpace.Opens.map f).sheafAdjunctionContinuous AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).unit.app F).hom.app (Opposite.op ⊤))) ((CategoryTheory.Sheaf.H.equiv₀ F CategoryTheory.Limits.isTerminalTop) x)

In degree zero, under the identifications of H⁰ with global sections, the inverse image map on cohomology is the unit F ⟶ f_* f⁻¹ F on global sections.