pentagon — Mathlib

English

The pentagon identity holds for the product associator in a category with binary products.

Русский

Пентагональное тождество выполняется для ассоциатора произведений.

LaTeX

$$$\text{pentagon}_{\text{prod}}(W,X,Y,Z)$$$

Lean4

@[reassoc]
theorem pentagon [HasBinaryProducts C] (W X Y Z : C) :
    prod.map (prod.associator W X Y).hom (𝟙 Z) ≫
        (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) (prod.associator X Y Z).hom =
      (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
  by simp

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