associator_naturality — Mathlib

English

The pentagon coherence diagram for the associator commutes: a standard coherence condition in any monoidal category.

Русский

Пентагональная диаграмма когерентности для ассоциатора в любом моноидальном категории сходится (диаграмма когерентности).

LaTeX

$$$(\\alpha_{W,X,Y})^{} \\;.$$$$

Lean4

theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) :=
  by
  ext : 1
  apply TensorProduct.ext_threefold
  intro x y z
  rfl

Похожие утверждения