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 #

theorem TopCat.Sheaf.pushforward_sheaf_of_sheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) {F : TopCat.Presheaf C X} (h : F.IsSheaf) :
(f _* F).IsSheaf

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

The pushforward functor.

Equations
Instances For

    Pushforward of sheaves is isomorphic (actually definitionally equal) to pushforward of presheaves.

    Equations
    Instances For
      @[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