symmetry — Mathlib

English

The braiding isomorphism for a binary product is symmetric: braiding(P,Q) = braiding(Q,P)^{-1} in the sense that their compositions yield the identity.

Русский

Перемешивание m для произведения симметрично: braiding(P,Q) = braiding(Q,P)^{-1} применимо к композициям.

LaTeX

$$$(prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = id$$$

Lean4

/-- The braiding isomorphism is symmetric. -/
@[reassoc]
theorem symmetry (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] :
    (prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _ :=
  (prod.braiding _ _).hom_inv_id

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