Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.associator_naturality

∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃))

Naturality of the associator isomorphism: (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ≃ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

11 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.MonoidalCategory