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)
:
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.