noncomputable def TopCat.Presheaf.pullbackPresheaf (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (𝒢 : Presheaf C Y) : Presheaf C X

The pullback presheaf of a presheaf 𝒢 on Y along a continuous map f : X ⟶ Y, defined via the pullback functor pullback C f.

theorem TopCat.Presheaf.pullbackPresheaf_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (𝒢 : Presheaf C Y) : pullbackPresheaf C f 𝒢 = (pullback C f).obj 𝒢

Unfolds pullbackPresheaf to the application of the pullback functor.

noncomputable def TopCat.Presheaf.pullbackAdj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) : pullback C f ⊣ pushforward C f

The pullback–pushforward adjunction f⁻¹ ⊣ f_* on presheaves with values in C.