symmetry — Mathlib

English

The braiding isomorphism is its own inverse: coprod.braiding P Q .hom ≫ coprod.braiding Q P .hom = id.

Русский

Браидинг-изоморфизм симметричен: coprod.braiding P Q .hom ≫ coprod.braiding Q P .hom = 𝟙.

LaTeX

$$$ (\\operatorname{coprod.braiding} P Q)^{\\mathrm{hom}} \\circ (\\operatorname{coprod.braiding} Q P)^{\\mathrm{hom}} = \\mathrm{Id} $$$

Lean4

/-- The braiding isomorphism is symmetric. -/
theorem symmetry (P Q : C) : (coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _ :=
  coprod.symmetry' _ _

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