Associativity of pullbacks

This file shows that pullbacks (and pushouts) are associative up to natural isomorphism.

def CategoryTheory.Limits.pullbackPullbackLeftIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) CategoryTheory.Limits.pullback.snd ⋯) ⋯)

(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.pullbackAssocIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) CategoryTheory.Limits.pullback.snd ⋯) ⋯)

(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback X₁ ×[Y₁] (X₂ ×[Y₂] X₃).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasPullback_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] : CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)

def CategoryTheory.Limits.pullbackPullbackRightIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) ⋯) CategoryTheory.Limits.pullback.snd ⋯)

X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.pullbackAssocSymmIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) ⋯) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) ⋯)

X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[Y₂] X₃.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasPullback_assoc_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄

noncomputable def CategoryTheory.Limits.pullbackAssoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄ ≅ CategoryTheory.Limits.pullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)

The canonical isomorphism (X₁ ×[Y₁] X₂) ×[Y₂] X₃ ≅ X₁ ×[Y₁] (X₂ ×[Y₂] X₃).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)

@[simp]

theorem CategoryTheory.Limits.pullbackAssoc_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasPushout_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] : CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasPushout_assoc_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄

noncomputable def CategoryTheory.Limits.pushoutAssoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ≅ CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)

The canonical isomorphism (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ ≅ X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h

@[simp]

theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.Limits.pushout.inl

@[simp]

theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)

@[simp]

theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr

@[simp]

theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h

@[simp]

theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.Limits.pushout.inr

@[simp]

theorem CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)

@[simp]

theorem CategoryTheory.Limits.inl_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl

@[simp]

theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)

@[simp]

theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl

@[simp]

theorem CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)

@[simp]

theorem CategoryTheory.Limits.inr_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inr