symmetry' — Mathlib

English

The associator in a category with binary products satisfies the pentagon identity for any four objects W, X, Y, Z; i.e., the usual coherence condition for associativity of products.

Русский

Ассоциатор в категории с двоичными произведениями удовлетворяет пентагон-условию для любых объектов W, X, Y, Z.

LaTeX

$$$\forall W X Y Z,\; \text{pentagon identity for } \prod$$$

Lean4

@[reassoc]
theorem symmetry' (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] :
    prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q) :=
  (prod.braiding _ _).hom_inv_id

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