Theorems · Theorem · category theory

CategoryTheory.IsPushout.map_iff

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F]
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F],
  CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i →
    (CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPushout f g h i)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.PreservesColimitCategoryTheory.Limits.ReflectsColimit