Theorems · Definition · category theory

TopCat.Presheaf.pushforwardEq

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} →
      {f g : X ⟶ Y} →
        f = g →
          (ℱ : TopCat.Presheaf C X) → (TopCat.Presheaf.pushforward C f).obj ℱ ≅ (TopCat.Presheaf.pushforward C g).obj ℱ

An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf along those maps.

Defined in

Mathlib.Topology.Sheaves.Presheaf

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category