Theorems · Theorem · category theory

TopCat.Presheaf.pullback_obj_obj_ext

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {Z : C} {f : X ⟶ Y} {F : TopCat.Presheaf C Y} (U : (TopologicalSpace.Opens ↑X)ᵒᵖ)
  {φ ψ : ((TopCat.Presheaf.pullback C f).obj F).obj U ⟶ Z},
  (∀ (V : TopologicalSpace.Opens ↑Y) (hV : Opposite.unop U ≤ (TopologicalSpace.Opens.map f).obj V),
      CategoryTheory.CategoryStruct.comp
          (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
          (CategoryTheory.CategoryStruct.comp
            (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) φ) =
        CategoryTheory.CategoryStruct.comp
          (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
          (CategoryTheory.CategoryStruct.comp
            (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) ψ)) →
    φ = ψ

Defined in

Mathlib.Topology.Sheaves.Stalks

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimits