Pullback of sheaf cohomology #

Let pb : Sheaf J Ab ⥤ Sheaf K Ab be an exact additive functor between categories of abelian sheaves on sites (C, J) and (D, K), together with a map c : ℤ_K ⟶ pb ℤ_J from the constant sheaf ℤ on (D, K) to the image of the constant sheaf ℤ on (C, J). Since Mathlib's sheaf cohomology Sheaf.H G n is Ext^n(ℤ_J, G), the pair (pb, c) induces Sheaf.H.pullback pb c G n : Hⁿ(C, G) →+ Hⁿ(D, pb G), the image of a class under pb precomposed with c. Without c an exact functor does not specify a map on cohomology.

The main case is a morphism of sites: a continuous functor u : C ⥤ D that is final (for instance representably flat) and whose sheaf pullback u^* = u.sheafPullback is exact. Then c is the inverse of the canonical isomorphism u^* ℤ_J ≅ ℤ_K (CategoryTheory.Functor.sheafPullbackConstantSheafIso), and Sheaf.H.pullback is the pullback Hⁿ(C, G) → Hⁿ(D, u^* G) along the morphism of sites. (The Stacks Project, Tag 08J6, constructs this pullback through the derived pushforward instead; that description is not formalised here.) In degree zero it is restriction of global sections: Sheaf.H.equiv₀_pullback_sheafPullback.

Main declarations #

CategoryTheory.Sheaf.H.pullback: the pullback of cohomology along (pb, c).
CategoryTheory.Sheaf.H.addEquiv₀_pullback: in degree zero, a map f : ℤ_J ⟶ G goes to c ≫ pb.map f.
CategoryTheory.Sheaf.H.pullback_naturality, pullback_id, pullback_comp_apply, pullback_δ, map_pullback_δ: naturality in the coefficient sheaf, the identity, composition, and compatibility with the connecting homomorphisms of a short exact sequence and its image under pb, also followed by a morphism of short exact sequences.
CategoryTheory.Sheaf.H.equiv₀_pullback_sheafPullback: for a morphism of sites, the pullback in degree zero is restriction of global sections along the unit of u^* ⊣ u_*.

Cohomology over objects and Mayer-Vietoris sequences #

The same construction applies to the cohomology Hⁿ(U, G) = Ext^n(ℤ[U], G) over an object U of the site, where ℤ[U] is the free abelian sheaf on U. Now the comparison is a natural transformation c : ℤ[u(-)] ⟶ pb ℤ[-] along a functor u : C ⥤ D; for a continuous functor u with pullback u^* it is CategoryTheory.Functor.freeYonedaSheafToSheafPullback. Given a morphism ψ : V ⟶ u(U), a class over U is sent by pb and precomposition with ℤ[V] ⟶ ℤ[u(U)] ⟶ pb ℤ[U] to a class over V. These maps commute with restriction on both sides, and they map the Mayer-Vietoris sequence of a Mayer-Vietoris square S in C to that of a Mayer-Vietoris square S' in D equipped with a morphism of squares from S' to the image of S under u. For the inverse image along a continuous map, this compares the Mayer-Vietoris sequences of two open subsets and of their preimages. Such comparisons drive Mayer-Vietoris inductions over the affine opens of a quasi-compact quasi-separated scheme, transporting a statement about the cohomology of quasi-coherent sheaves from affine opens to the whole scheme.

CategoryTheory.Sheaf.H'.pullback: the pullback Hⁿ(U, G) ⟶ Hⁿ(V, pb G) along ψ.
CategoryTheory.Sheaf.H'.pullback_naturality: compatibility with coefficient morphisms.
CategoryTheory.Sheaf.H'.pullback_comp_map, map_comp_pullback: compatibility with restriction.
CategoryTheory.Sheaf.H'.addEquiv₀_pullback: in degree zero, the pullback of the class of g : ℤ[U] ⟶ G is the class of ℤ[V] ⟶ ℤ[u(U)] ⟶ pb ℤ[U] ⟶ pb G.
CategoryTheory.Sheaf.H'.toBiprod_comp_pullback, fromBiprod_comp_pullback, δ_comp_pullback, and mayerVietorisSequencePullback: the morphism between the Mayer-Vietoris sequences, with components mayerVietorisSequencePullback_app_zero through mayerVietorisSequencePullback_app_five.
CategoryTheory.Sheaf.H'.cohomologyZeroSectionsEquiv_pullback_sheafPullback: for a morphism of sites, the pullback in degree zero is the unit of u^* ⊣ u_* on sections over U, followed by restriction along ψ.