Theorems · Definition · category theory

CategoryTheory.Limits.pushout.desc

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPushout f g] →
            (h : Y ⟶ W) →
              (k : Z ⟶ W) →
                autoParam (CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
                    CategoryTheory.Limits.pushout.desc._auto_1 →
                  (CategoryTheory.Limits.pushout f g ⟶ W)

A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism pushout.desc : pushout f g ⟶ W.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Cited by

46 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushout