reverseBraiding_eq — Mathlib

English

In a symmetric category, the reverse braiding coincides with the symmetry braiding; more precisely, reverseBraiding C equals i.toBraidedCategory, which expresses that the braiding is symmetric (β_{X,Y} = β_{Y,X}^{-1}).

Русский

В симметричной категории обратный браидинг совпадает с браидингом, порождаемым симметрией; то есть reverseBraiding C равен i.toBraidedCategory, что эквивалентно тому, что braiding симметричен (β_{X,Y} = β_{Y,X}^{-1}).

LaTeX

$$$ reverseBraiding\\, C = i.toBraidedCategory $$$

Lean4

theorem reverseBraiding_eq (C : Type u₁) [Category.{v₁} C] [MonoidalCategory C] [i : SymmetricCategory C] :
    reverseBraiding C = i.toBraidedCategory :=
  by
  dsimp only [reverseBraiding]
  congr
  funext X Y
  exact Iso.ext (braiding_swap_eq_inv_braiding Y X).symm

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