# 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} {X : TopCat} {Y : TopCat} (f : X Y) {F : } (h : F.IsSheaf) :
(f _* F).IsSheaf

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

def TopCat.Sheaf.pushforward (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y) :

The pushforward functor.

Equations
• = .sheafPushforwardContinuous C
Instances For
theorem TopCat.Sheaf.pushforward_forget (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y) :
().comp () = ().comp
def TopCat.Sheaf.pushforwardForgetIso (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y) :
().comp () ().comp

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

Equations
Instances For
@[simp]
theorem TopCat.Sheaf.pushforward_obj_val {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (F : ) :
(().obj F).val = f _* F.val
@[simp]
theorem TopCat.Sheaf.pushforward_map {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) {F : } {F' : } (α : F F') :
(().map α).val = .map α.val
def TopCat.Sheaf.pullback {X : TopCat} {Y : TopCat} (A : Type u_1) [] [.ReflectsIsomorphisms] (f : X Y) :

The pullback functor.

Equations
• = .sheafPullback A
Instances For
theorem TopCat.Sheaf.pullback_eq {X : TopCat} {Y : TopCat} (A : Type u_1) [] [.ReflectsIsomorphisms] (f : X Y) :
= ().comp (().comp )
def TopCat.Sheaf.pullbackIso {X : TopCat} {Y : TopCat} (A : Type u_1) [] [.ReflectsIsomorphisms] (f : X Y) :
().comp (().comp )

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 : TopCat} {Y : TopCat} (A : Type u_1) [] [.ReflectsIsomorphisms] (f : X Y) :

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

Equations
• = .sheafAdjunctionContinuous A
Instances For
instance TopCat.Sheaf.instIsLeftAdjointPullback {X : TopCat} {Y : TopCat} (f : X Y) (A : Type u_1) [] [.ReflectsIsomorphisms] :
().IsLeftAdjoint
Equations
• =
instance TopCat.Sheaf.instIsRightAdjointPushforward {X : TopCat} {Y : TopCat} (f : X Y) (A : Type u_1) [] [.ReflectsIsomorphisms] :
().IsRightAdjoint
Equations
• =