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.presheaf.sheaf_condition_pairwise_intersections.map_diagram
{X Y : Top}
(f : X ⟶ Y)
⦃ι : Type w⦄
{U : ι → topological_space.opens ↥Y} :
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.map_cocone
{X Y : Top}
(f : X ⟶ Y)
⦃ι : Type w⦄
{U : ι → topological_space.opens ↥Y} :
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.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_pairwise_intersections) :
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) :
The pushforward of a sheaf (by a continuous map) is a sheaf.
The pushforward functor.