mathlib documentation


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.

TODO: pullback for presheaves and sheaves

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

The pushforward functor.