Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Associativity of pullbacks #

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

source
def CategoryTheory.Limits.pullbackPullbackLeftIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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.
Instances For
    source
    def CategoryTheory.Limits.pullbackAssocIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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.
    Instances For
      source
      theorem CategoryTheory.Limits.hasPullback_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₂)
      source
      def CategoryTheory.Limits.pullbackPullbackRightIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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.
      Instances For
        source
        def CategoryTheory.Limits.pullbackAssocSymmIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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.
        Instances For
          source
          theorem CategoryTheory.Limits.hasPullback_assoc_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₄
          source
          noncomputable def CategoryTheory.Limits.pullbackAssoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₂)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₂)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₂)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₄
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₄)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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₄)
            source
            @[simp]
            theorem CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ 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)
            source
            def CategoryTheory.Limits.pushoutPushoutLeftIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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.
            Instances For
              source
              def CategoryTheory.Limits.pushoutAssocIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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.
              Instances For
                source
                theorem CategoryTheory.Limits.hasPushout_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄))
                source
                def CategoryTheory.Limits.pushoutPushoutRightIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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.
                Instances For
                  source
                  def CategoryTheory.Limits.pushoutAssocSymmIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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.
                  Instances For
                    source
                    theorem CategoryTheory.Limits.hasPushout_assoc_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄
                    source
                    noncomputable def CategoryTheory.Limits.pushoutAssoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄))
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄)))
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inl_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inr_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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₄)))
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ 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)