Theorems · Theorem · category theory

TopCat.Presheaf.toPushforwardOfIso_app

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C X}
  {𝒢 : TopCat.Presheaf C Y} (H₂ : (TopCat.Presheaf.pushforward C H₁.hom).obj ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U =
    CategoryTheory.CategoryStruct.comp (ℱ.map (CategoryTheory.eqToHom ⋯))
      (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U))))

Defined in

Mathlib.Topology.Sheaves.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category