Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        (X₁ X₂ X₃ : CategoryTheory.Arrow C) →
          [CategoryTheory.Limits.PreservesColimit
                (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                (CategoryTheory.MonoidalCategory.tensorRight X₃.left)] →
            [CategoryTheory.Limits.PreservesColimit
                  (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                  (CategoryTheory.MonoidalCategory.tensorRight X₃.right)] →
              [CategoryTheory.Limits.PreservesColimit
                    (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
                    (CategoryTheory.MonoidalCategory.tensorLeft X₁.left)] →
                [CategoryTheory.Limits.PreservesColimit
                      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
                      (CategoryTheory.MonoidalCategory.tensorLeft X₁.right)] →
                  ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃

The pushout-product is associative: (X₁ □ X₂) □ X₃ ≅ X₁ □ X₂ □ X₃.

Defined in

Mathlib.CategoryTheory.Monoidal.PushoutProduct

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushoutsCategoryTheory.MonoidalCategoryCategoryTheory.Limits.PreservesColimitCategoryTheory.Limits.PreservesColimitCategoryTheory.Limits.PreservesColimitCategoryTheory.Limits.PreservesColimit