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

Equations

• TopCat.Sheaf.pushforward C f = CategoryTheory.Functor.sheafPushforwardContinuous (TopologicalSpace.Opens.map f) C (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)

theorem TopCat.Sheaf.pushforward_forget (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor.comp (TopCat.Sheaf.pushforward C f) (TopCat.Sheaf.forget C Y) = CategoryTheory.Functor.comp (TopCat.Sheaf.forget C X) (TopCat.Presheaf.pushforward C f)

def TopCat.Sheaf.pushforwardForgetIso (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor.comp (TopCat.Sheaf.pushforward C f) (TopCat.Sheaf.forget C Y) ≅ CategoryTheory.Functor.comp (TopCat.Sheaf.forget C X) (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 (CategoryTheory.Functor.comp (TopCat.Sheaf.pushforward C f) (TopCat.Sheaf.forget C Y))

@[simp]

theorem TopCat.Sheaf.pushforward_obj_val {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (F : TopCat.Sheaf C X) : ((TopCat.Sheaf.pushforward C f).toPrefunctor.obj F).val = f _* F.val

@[simp]

theorem TopCat.Sheaf.pushforward_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {F : TopCat.Sheaf C X} {F' : TopCat.Sheaf C X} (α : F ⟶ F') : ((TopCat.Sheaf.pushforward C f).toPrefunctor.map α).val = (TopCat.Presheaf.pushforward C f).toPrefunctor.map α.val

def TopCat.Sheaf.pullback {X : TopCat} {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.ReflectsIsomorphisms (CategoryTheory.forget A)] (f : X ⟶ Y) : CategoryTheory.Functor (TopCat.Sheaf A Y) (TopCat.Sheaf A X)

The pullback functor.

Equations

• TopCat.Sheaf.pullback A f = CategoryTheory.Functor.sheafPullback (TopologicalSpace.Opens.map f) A (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)

theorem TopCat.Sheaf.pullback_eq {X : TopCat} {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.ReflectsIsomorphisms (CategoryTheory.forget A)] (f : X ⟶ Y) : TopCat.Sheaf.pullback A f = CategoryTheory.Functor.comp (TopCat.Sheaf.forget A Y) (CategoryTheory.Functor.comp (TopCat.Presheaf.pullback A f) (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) A))

def TopCat.Sheaf.pullbackIso {X : TopCat} {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.ReflectsIsomorphisms (CategoryTheory.forget A)] (f : X ⟶ Y) : TopCat.Sheaf.pullback A f ≅ CategoryTheory.Functor.comp (TopCat.Sheaf.forget A Y) (CategoryTheory.Functor.comp (TopCat.Presheaf.pullback A f) (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

• TopCat.Sheaf.pullbackIso A f = CategoryTheory.Iso.refl (TopCat.Sheaf.pullback A f)

def TopCat.Sheaf.pullbackPushforwardAdjunction {X : TopCat} {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.ReflectsIsomorphisms (CategoryTheory.forget A)] (f : X ⟶ Y) : TopCat.Sheaf.pullback A f ⊣ TopCat.Sheaf.pushforward A f

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

Equations

• One or more equations did not get rendered due to their size.

instance TopCat.Sheaf.instIsLeftAdjointSheafSheafCatPullback {X : TopCat} {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.ReflectsIsomorphisms (CategoryTheory.forget A)] : CategoryTheory.IsLeftAdjoint (TopCat.Sheaf.pullback A f)

Equations

• TopCat.Sheaf.instIsLeftAdjointSheafSheafCatPullback f A = { right := TopCat.Sheaf.pushforward A f, adj := TopCat.Sheaf.pullbackPushforwardAdjunction A f }

instance TopCat.Sheaf.instIsRightAdjointSheafSheafCatPushforward {X : TopCat} {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.ReflectsIsomorphisms (CategoryTheory.forget A)] : CategoryTheory.IsRightAdjoint (TopCat.Sheaf.pushforward A f)

Equations

• TopCat.Sheaf.instIsRightAdjointSheafSheafCatPushforward f A = { left := TopCat.Sheaf.pullback A f, adj := TopCat.Sheaf.pullbackPushforwardAdjunction A f }