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 TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram {X : TopCat} {Y : TopCat} (f : X ⟶ Y) ⦃ι : Type w⦄ {U : ι → TopologicalSpace.Opens ↑Y} : CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U) (TopologicalSpace.Opens.map f) = CategoryTheory.Pairwise.diagram ((TopologicalSpace.Opens.map f).toPrefunctor.obj ∘ U)

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.mapCocone {X : TopCat} {Y : TopCat} (f : X ⟶ Y) ⦃ι : Type w⦄ {U : ι → TopologicalSpace.Opens ↑Y} : HEq ((TopologicalSpace.Opens.map f).mapCocone (CategoryTheory.Pairwise.cocone U)) (CategoryTheory.Pairwise.cocone ((TopologicalSpace.Opens.map f).toPrefunctor.obj ∘ U))

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf.IsSheafPairwiseIntersections F) : TopCat.Presheaf.IsSheafPairwiseIntersections (f _* F)

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 : TopCat.Presheaf.IsSheaf F) : TopCat.Presheaf.IsSheaf (f _* F)

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

def TopCat.Sheaf.pushforward {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor (TopCat.Sheaf C X) (TopCat.Sheaf C Y)

The pushforward functor.