Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.pushoutDesc_inl_inr

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange] {S S' X Y : C} (f : S ⟶ S') {v₁₂ : S ⟶ X} {v₂₂ : S ⟶ Y} {g : Y ⟶ X}
  (hv₁₂ : v₁₂ = CategoryTheory.CategoryStruct.comp v₂₂ g) [inst_2 : CategoryTheory.Limits.HasPushout v₁₂ f]
  [inst_3 : CategoryTheory.Limits.HasPushout v₂₂ f],
  P g →
    P
      (CategoryTheory.Limits.pushout.desc
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.pushout.inl v₁₂ f))
        (CategoryTheory.Limits.pushout.inr v₁₂ f) ⋯)

Defined in

Mathlib.CategoryTheory.MorphismProperty.Limits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderCobaseChangeCategoryTheory.Limits.HasPushoutCategoryTheory.Limits.HasPushout