mathlib documentation


functors between categories of sheaves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

TODO: pullback for presheaves and sheaves

theorem Top.sheaf.pushforward_sheaf_of_sheaf {C : Type u} [category_theory.category C] {X Y : Top} (f : X Y) {F : Top.presheaf C X} (h : F.is_sheaf) :
(f _* F).is_sheaf

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

def Top.sheaf.pushforward {C : Type u} [category_theory.category C] {X Y : Top} (f : X Y) :

The pushforward functor.