pentagon — Mathlib

English

The associator satisfies the pentagon axiom, expressing coherence of associativity for quadruples of objects.

Русский

Ассоциатор удовлетворяет пентагональному тождению, выражающему когерентность ассоциативности для четырех объектов.

LaTeX

$$$\text{pentagon identity: } (a\otimes b)\otimes c \Rightarrow a\otimes (b\otimes c) \text{ commute}$$$

Lean4

theorem pentagon (W X Y Z : Dial C) :
    (tensorHom (associator W X Y).hom (𝟙 Z)) ≫
        (associator W (tensorObj X Y) Z).hom ≫ (tensorHom (𝟙 W) (associator X Y Z).hom) =
      (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom :=
  by ext <;> simp

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