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} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] :
IsLimit (PullbackCone.mk (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (pullback.lift (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (pullback.snd f₁ f₂)) (pullback.snd (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) ⋯) ⋯)

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

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

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

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

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

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

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

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

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (pullback.fst f₁ f₂)) = pullback.fst f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₁ ⟶ Z) :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (CategoryStruct.comp (pullback.fst f₁ f₂) h)) = CategoryStruct.comp (pullback.fst f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) h
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_hom_fst {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).hom (pullback.fst f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (pullback.fst f₁ f₂)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₁ ⟶ Z) :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryStruct.comp (pullback.fst f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) h) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (CategoryStruct.comp (pullback.fst f₁ f₂) h)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (pullback.fst f₃ f₄)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (pullback.snd f₁ f₂)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₂ ⟶ Z) :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (CategoryStruct.comp (pullback.fst f₃ f₄) h)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (CategoryStruct.comp (pullback.snd f₁ f₂) h)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (pullback.snd f₃ f₄)) = pullback.snd (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₃ ⟶ Z) :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (CategoryStruct.comp (pullback.snd f₃ f₄) h)) = CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) h
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (pullback.snd f₁ f₂)) = CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (pullback.fst f₃ f₄)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₂ ⟶ Z) :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) (CategoryStruct.comp (pullback.snd f₁ f₂) h)) = CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (CategoryStruct.comp (pullback.fst f₃ f₄) h)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_inv_snd {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).inv (pullback.snd (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) = CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (pullback.snd f₃ f₄)
                      source
                      @[simp]
                      theorem CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁) (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄] [HasPullback (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄] [HasPullback f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)] {Z : C} (h : X₃ ⟶ Z) :
                      CategoryStruct.comp (pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd f₁ f₂) f₃) f₄) h) = CategoryStruct.comp (pullback.snd f₁ (CategoryStruct.comp (pullback.fst f₃ f₄) f₂)) (CategoryStruct.comp (pullback.snd f₃ f₄) h)
                      source
                      def CategoryTheory.Limits.pushoutPushoutLeftIsPushout {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] :
                      IsColimit (PushoutCocone.mk (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (pushout.desc (CategoryStruct.comp (pushout.inr g₁ g₂) (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄)) (pushout.inr (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) ⋯) ⋯)

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

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

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

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

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

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

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

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

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

                                      Equations
                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] :
                                          CategoryStruct.comp (pushout.inl g₁ g₂) (CategoryStruct.comp (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (pushoutAssoc g₁ g₂ g₃ g₄).hom) = pushout.inl g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] {Z : C} (h : pushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄)) ⟶ Z) :
                                          CategoryStruct.comp (pushout.inl g₁ g₂) (CategoryStruct.comp (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (CategoryStruct.comp (pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryStruct.comp (pushout.inl g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) h
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] :
                                          CategoryStruct.comp (pushout.inr g₁ g₂) (CategoryStruct.comp (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryStruct.comp (pushout.inl g₃ g₄) (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄)))
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] {Z : C} (h : pushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄)) ⟶ Z) :
                                          CategoryStruct.comp (pushout.inr g₁ g₂) (CategoryStruct.comp (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (CategoryStruct.comp (pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryStruct.comp (pushout.inl g₃ g₄) (CategoryStruct.comp (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) h)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] :
                                          CategoryStruct.comp (pushout.inr g₃ g₄) (CategoryStruct.comp (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) (pushoutAssoc g₁ g₂ g₃ g₄).inv) = pushout.inr (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] {Z : C} (h : pushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄ ⟶ Z) :
                                          CategoryStruct.comp (pushout.inr g₃ g₄) (CategoryStruct.comp (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) (CategoryStruct.comp (pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryStruct.comp (pushout.inr (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) h
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inl_pushoutAssoc_inv {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] :
                                          CategoryStruct.comp (pushout.inl g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) (pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryStruct.comp (pushout.inl g₁ g₂) (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] {Z : C} (h : pushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄ ⟶ Z) :
                                          CategoryStruct.comp (pushout.inl g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) (CategoryStruct.comp (pushoutAssoc g₁ g₂ g₃ g₄).inv h) = CategoryStruct.comp (pushout.inl g₁ g₂) (CategoryStruct.comp (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) h)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] :
                                          CategoryStruct.comp (pushout.inl g₃ g₄) (CategoryStruct.comp (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) (pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryStruct.comp (pushout.inr g₁ g₂) (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] {Z : C} (h : pushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄ ⟶ Z) :
                                          CategoryStruct.comp (pushout.inl g₃ g₄) (CategoryStruct.comp (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) (CategoryStruct.comp (pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryStruct.comp (pushout.inr g₁ g₂) (CategoryStruct.comp (pushout.inl (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) h)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inr_pushoutAssoc_hom {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] :
                                          CategoryStruct.comp (pushout.inr (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryStruct.comp (pushout.inr g₃ g₄) (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄)))
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂) (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄] [HasPushout (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄] [HasPushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))] {Z : C} (h : pushout g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄)) ⟶ Z) :
                                          CategoryStruct.comp (pushout.inr (CategoryStruct.comp g₃ (pushout.inr g₁ g₂)) g₄) (CategoryStruct.comp (pushoutAssoc g₁ g₂ g₃ g₄).hom h) = CategoryStruct.comp (pushout.inr g₃ g₄) (CategoryStruct.comp (pushout.inr g₁ (CategoryStruct.comp g₂ (pushout.inl g₃ g₄))) h)