Theorems · Definition · category theory

CategoryTheory.Limits.pullbackAssoc

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ Y₂ : C} →
      (f₁ : X₁ ⟶ Y₁) →
        (f₂ : X₂ ⟶ Y₁) →
          (f₃ : X₂ ⟶ Y₂) →
            (f₄ : X₃ ⟶ Y₂) →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPullback
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄] →
                    [inst_4 :
                        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₃).

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Cited by

23 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback