Theorems · Definition · category theory

CategoryTheory.Limits.pushoutAssocIsPushout

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Z₁ Z₂ : C} →
      (g₁ : Z₁ ⟶ X₁) →
        (g₂ : Z₁ ⟶ X₂) →
          (g₃ : Z₂ ⟶ X₂) →
            (g₄ : Z₂ ⟶ X₃) →
              [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPushout
                        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄] →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.PushoutCocone.mk
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂)
                          (CategoryTheory.Limits.pushout.inl
                            (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄))
                        (CategoryTheory.Limits.pushout.desc
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
                            (CategoryTheory.Limits.pushout.inl
                              (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄))
                          (CategoryTheory.Limits.pushout.inr
                            (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
                          ⋯)
                        ⋯)

(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushoutCategoryTheory.Limits.HasPushoutCategoryTheory.Limits.HasPushout