Theorems · Definition · category theory

TopCat.Presheaf.pullbackInvIsoPushforwardHom

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} → (H : X ≅ Y) → TopCat.Presheaf.pullback C H.inv ≅ TopCat.Presheaf.pushforward C H.hom

Pulling back along the inverse of a homeomorphism is the same as pushing forward along it.

Defined in

Mathlib.Topology.Sheaves.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimits