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.
Main definitions #
TopCat.Sheaf.pushforward: The pushforward functor between sheaf categories over topological spaces.TopCat.Sheaf.pullback: The pullback functor between sheaf categories over topological spaces.TopCat.Sheaf.pullbackPushforwardAdjunction: The adjunction between pullback and pushforward for sheaves on topological spaces.
theorem
TopCat.Sheaf.pushforward_sheaf_of_sheaf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : TopCat}
(f : X ⟶ Y)
{F : TopCat.Presheaf C X}
(h : F.IsSheaf)
:
((TopCat.Presheaf.pushforward C f).obj F).IsSheaf
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 Y : TopCat}
(f : X ⟶ Y)
:
CategoryTheory.Functor (TopCat.Sheaf C X) (TopCat.Sheaf C Y)
The pushforward functor.
Equations
- TopCat.Sheaf.pushforward C f = (TopologicalSpace.Opens.map f).sheafPushforwardContinuous C (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)
Instances For
theorem
TopCat.Sheaf.pushforward_forget
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X Y : TopCat}
(f : X ⟶ Y)
:
(TopCat.Sheaf.pushforward C f).comp (TopCat.Sheaf.forget C Y) = (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.pushforward C f)
def
TopCat.Sheaf.pushforwardForgetIso
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X Y : TopCat}
(f : X ⟶ Y)
:
(TopCat.Sheaf.pushforward C f).comp (TopCat.Sheaf.forget C Y) ≅ (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.pushforward C f)
Pushforward of sheaves is isomorphic (actually definitionally equal) to pushforward of presheaves.
Equations
- TopCat.Sheaf.pushforwardForgetIso C f = CategoryTheory.Iso.refl ((TopCat.Sheaf.pushforward C f).comp (TopCat.Sheaf.forget C Y))
Instances For
@[simp]
theorem
TopCat.Sheaf.pushforward_obj_val
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : TopCat}
(f : X ⟶ Y)
(F : TopCat.Sheaf C X)
:
((TopCat.Sheaf.pushforward C f).obj F).val = (TopCat.Presheaf.pushforward C f).obj F.val
@[simp]
theorem
TopCat.Sheaf.pushforward_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : TopCat}
(f : X ⟶ Y)
{F F' : TopCat.Sheaf C X}
(α : F ⟶ F')
:
((TopCat.Sheaf.pushforward C f).map α).val = (TopCat.Presheaf.pushforward C f).map α.val
def
TopCat.Sheaf.pullback
{X Y : TopCat}
(A : Type u_1)
[CategoryTheory.Category.{w, u_1} A]
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
(f : X ⟶ Y)
:
CategoryTheory.Functor (TopCat.Sheaf A Y) (TopCat.Sheaf A X)
The pullback functor.
Equations
- TopCat.Sheaf.pullback A f = (TopologicalSpace.Opens.map f).sheafPullback A (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)
Instances For
theorem
TopCat.Sheaf.pullback_eq
{X Y : TopCat}
(A : Type u_1)
[CategoryTheory.Category.{w, u_1} A]
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
(f : X ⟶ Y)
:
TopCat.Sheaf.pullback A f = (TopCat.Sheaf.forget A Y).comp
((TopCat.Presheaf.pullback A f).comp (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) A))
def
TopCat.Sheaf.pullbackIso
{X Y : TopCat}
(A : Type u_1)
[CategoryTheory.Category.{w, u_1} A]
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
(f : X ⟶ Y)
:
TopCat.Sheaf.pullback A f ≅ (TopCat.Sheaf.forget A Y).comp
((TopCat.Presheaf.pullback A f).comp (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) A))
The pullback of a sheaf is isomorphic (actually definitionally equal) to the sheafification of the pullback as a presheaf.
Equations
Instances For
def
TopCat.Sheaf.pullbackPushforwardAdjunction
{X Y : TopCat}
(A : Type u_1)
[CategoryTheory.Category.{w, u_1} A]
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
(f : X ⟶ Y)
:
The adjunction between pullback and pushforward for sheaves on topological spaces.
Equations
- TopCat.Sheaf.pullbackPushforwardAdjunction A f = (TopologicalSpace.Opens.map f).sheafAdjunctionContinuous A (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)
Instances For
instance
TopCat.Sheaf.instIsLeftAdjointPullback
{X Y : TopCat}
(f : X ⟶ Y)
(A : Type u_1)
[CategoryTheory.Category.{w, u_1} A]
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
:
(TopCat.Sheaf.pullback A f).IsLeftAdjoint
Equations
- ⋯ = ⋯
instance
TopCat.Sheaf.instIsRightAdjointPushforward
{X Y : TopCat}
(f : X ⟶ Y)
(A : Type u_1)
[CategoryTheory.Category.{w, u_1} A]
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
:
(TopCat.Sheaf.pushforward A f).IsRightAdjoint
Equations
- ⋯ = ⋯