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₂) f₃) f₄] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.snd f₁ f₂)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) ⋯) ⋯)

(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₂) f₃) f₄] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.fst f₁ f₂)) (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.snd f₁ f₂)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) ⋯) ⋯)

(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₂) f₃) f₄] : CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) 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₃ f₄) f₂)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.fst f₃ f₄)) ⋯) (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) ⋯)

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₃ f₄) f₂)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.fst f₃ f₄)) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.snd f₃ f₄)) ⋯)

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₃ f₄) f₂)] : CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) 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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄ ≅ CategoryTheory.Limits.pullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) 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 {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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : 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 f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.fst f₁ f₂)) = CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)

@[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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) 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 f₁ f₂) f₃) f₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₁ f₂) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) 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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.fst f₁ f₂)

@[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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₁ f₂) 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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.fst f₃ f₄)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.snd f₁ f₂)

@[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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) 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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.snd f₃ f₄)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄

@[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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₃ f₄) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) 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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : 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 f₁ f₂) f₃) f₄) (CategoryTheory.Limits.pullback.snd f₁ f₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.fst f₃ f₄)

@[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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) 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 f₁ f₂) f₃) f₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) 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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.Limits.pullback.snd f₃ f₄)

@[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₂) f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₃ f₄) h)

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₁ g₂)) g₄] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (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₂) ×[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₁ 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₃).

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₁ g₂)) g₄] : CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))

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 g₃ g₄))] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.desc (CategoryTheory.Limits.pushout.inl g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄) (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))) ⋯) (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) ⋯)

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 g₃ g₄))] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.desc (CategoryTheory.Limits.pushout.inl g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄) (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄) (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))) ⋯)

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 g₃ g₄))] : CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) 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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ≅ CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))

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 {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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.Limits.pushout.inl g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))

@[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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) 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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄) (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))

@[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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) 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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄

@[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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) 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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂) (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)

@[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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) 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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂) (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)

@[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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) 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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄) (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))

@[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₁ g₂)) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))) h)