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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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
          • 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} [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
            • One or more equations did not get rendered due to their size.
            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
              • One or more equations did not get rendered due to their size.
              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
                • One or more equations did not get rendered due to their size.
                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
                  • One or more equations did not get rendered due to their size.
                  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
                    • 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} [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)