Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_inv_left

∀ {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)
  [inst_3 :
    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)]
  [inst_4 :
    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)]
  [inst_5 :
    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)]
  [inst_6 :
    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)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator X₁ X₂ X₃).inv.left =
    CategoryTheory.Limits.pushout.desc
      (CategoryTheory.CategoryStruct.comp ⋯.isoPushout.hom
        (CategoryTheory.Limits.colimit.desc
          (CategoryTheory.Limits.span
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left))
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom)))
          ((CategoryTheory.Limits.Cocone.precompose
                (CategoryTheory.Limits.spanExt
                    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.left X₃.left).symm
                    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.right X₃.left).symm
                    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.left X₃.right).symm ⋯ ⋯).hom).obj
            (CategoryTheory.Limits.PushoutCocone.mk
              (CategoryTheory.Limits.pushout.inl
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  (CategoryTheory.Limits.pushout.desc
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right X₂.hom)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.right) ⋯)
                  X₃.left)
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
                  (CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                  X₃.hom))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                  X₃.right)
                (CategoryTheory.Limits.pushout.inr
                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                    (CategoryTheory.Limits.pushout.desc
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right X₂.hom)
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.right) ⋯)
                    X₃.left)
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
                    (CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                    X₃.hom)))
              ⋯))))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.right X₃.right).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
            X₃.right)
          (CategoryTheory.Limits.pushout.inr
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.Limits.pushout.desc (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right X₂.hom)
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.right) ⋯)
              X₃.left)
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
              (CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
              X₃.hom))))
      ⋯

Defined in

Mathlib.CategoryTheory.Monoidal.PushoutProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

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