pentagon_inv_inv_hom — Mathlib

English

The standard pentagon diagram commutes in any monoidal category, expressing associativity coherence for four objects W, X, Y, Z.

Русский

Стандартная пентагональная диаграмма когерентности в любой моноидальной категории: ассоциативность на четырех объектах W, X, Y, Z согласована.

LaTeX

$$$(\\alpha_W (X \\otimes Y) Z)^{\\mathrm{inv}} \\circ ((\\alpha_W X Y)^{\\mathrm{inv}} \\otimes Id_Z) \\circ (\\alpha_{(W \\otimes X) Y Z})^{\\mathrm{hom}} = (Id_W \\otimes (\\alpha_{X Y Z})^{\\mathrm{hom}}) \\circ (\\alpha_{W X (Y \\otimes Z)})^{\\mathrm{inv}}$$$

Lean4

@[reassoc]
theorem pentagon_inv_inv_hom (W X Y Z : C) :
    (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ₘ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom =
      (𝟙 W ⊗ₘ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv :=
  by simp

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