Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.iff_of_isPushout

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y A : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q],
  CategoryTheory.IsPushout f g inl inr → Q f → (P inl ↔ P g)

Defined in

Mathlib.CategoryTheory.MorphismProperty.Descent

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderCobaseChangeCategoryTheory.MorphismProperty.CodescendsAlong