Documentation

Mathlib.Topology.Sheaves.Functors

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 #

source
theorem TopCat.Sheaf.pushforward_sheaf_of_sheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {F : Presheaf C X} (h : F.IsSheaf) :
((Presheaf.pushforward C f).obj F).IsSheaf

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

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

The pushforward functor.

Equations
    Instances For
      source
      theorem TopCat.Sheaf.pushforward_forget (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) :
      (pushforward C f).comp (forget C Y) = (forget C X).comp (Presheaf.pushforward C f)
      source
      def TopCat.Sheaf.pushforwardForgetIso (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) :
      (pushforward C f).comp (forget C Y) ≅ (forget C X).comp (Presheaf.pushforward C f)

      Pushforward of sheaves is isomorphic (actually definitionally equal) to pushforward of presheaves.

      Equations
        Instances For
          source
          @[simp]
          theorem TopCat.Sheaf.pushforward_obj_val {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) (F : Sheaf C X) :
          ((pushforward C f).obj F).val = (Presheaf.pushforward C f).obj F.val
          source
          @[simp]
          theorem TopCat.Sheaf.pushforward_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {F F' : Sheaf C X} (α : F ⟶ F') :
          ((pushforward C f).map α).val = (Presheaf.pushforward C f).map α.val
          source
          def TopCat.Sheaf.pullback {X Y : TopCat} (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [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 (Sheaf A Y) (Sheaf A X)

          The pullback functor.

          Equations
            Instances For
              source
              def TopCat.Sheaf.pullbackIso {X Y : TopCat} (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [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) :
              pullback A f ≅ (forget A Y).comp ((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
                  source
                  def TopCat.Sheaf.pullbackPushforwardAdjunction {X Y : TopCat} (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [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) :
                  pullback A f ⊣ pushforward A f

                  The adjunction between pullback and pushforward for sheaves on topological spaces.

                  Equations
                    Instances For
                      source
                      instance TopCat.Sheaf.instIsLeftAdjointPullback {X Y : TopCat} (f : X ⟶ Y) (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms] :
                      (pullback A f).IsLeftAdjoint
                      source
                      instance TopCat.Sheaf.instIsRightAdjointPushforward {X Y : TopCat} (f : X ⟶ Y) (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms] :
                      (pushforward A f).IsRightAdjoint