Documentation

Mathlib.Topology.Sheaves.Functors

functors between categories of sheaves #

Show that the pushforward of a sheaf is a sheaf, and define the pushforward functor from the category of C-valued sheaves on X to that of sheaves on Y, given a continuous map between topological spaces X and Y.

Main definitions #

The pushforward of a sheaf (by a continuous map) is a sheaf.

@[simp]
theorem TopCat.Sheaf.pushforward_obj_val {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) (F : TopCat.Sheaf C X) :
((TopCat.Sheaf.pushforward C f).obj F).val = f _* F.val
@[simp]
theorem TopCat.Sheaf.pushforward_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) {F : TopCat.Sheaf C X} {F' : TopCat.Sheaf C X} (α : F F') :
((TopCat.Sheaf.pushforward C f).map α).val = (TopCat.Presheaf.pushforward C f).map α.val