Theorems · Definition · category theory

TopCat.Presheaf.pullbackPushforwardAdjunction

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

The pullback and pushforward along a continuous map are adjoint to each other.

Defined in

Mathlib.Topology.Sheaves.Presheaf

Cited by

9 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimits