Theorems · Theorem · category theory

CategoryTheory.Subobject.map_pullback

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W} [inst_2 : CategoryTheory.Mono h]
  [inst_3 : CategoryTheory.Mono g]
  (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
  (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm)) (p : CategoryTheory.Subobject Y),
  (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.pullback f).obj p) =
    (CategoryTheory.Subobject.pullback k).obj ((CategoryTheory.Subobject.map h).obj p)

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.MonoCategoryTheory.Mono