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
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.map_diagram
{X Y : Top}
(f : X ⟶ Y)
⦃ι : Type v⦄
{U : ι → topological_space.opens ↥Y} :
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.map_cocone
{X Y : Top}
(f : X ⟶ Y)
⦃ι : Type v⦄
{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)
[category_theory.limits.has_products C]
{F : Top.presheaf C X}
(h : 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}
[category_theory.limits.has_products C]
(f : X ⟶ Y) :
The pushforward functor.