Theorems · Definition · category theory

CategoryTheory.MonoidalCategoryStruct.associator

{C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      (X Y Z : C) →
        CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ≅
          CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)

The associator isomorphism (X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

667 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 5 definitions · uses no axioms

Assumes

CategoryTheory.MonoidalCategoryStruct