braiding_swap_eq_inv_braiding — Mathlib

English

Let C be a symmetric monoidal category. For any objects X and Y, the braiding is its own inverse in the sense that the braiding from Y to X is the inverse of the braiding from X to Y; equivalently, (β_{Y,X}).hom = (β_{X,Y}).inv.

Русский

Пусть C — симметричная моноидальная категория. Для любых объектов X и Y braiding между Y и X является обратной braiding между X и Y; то есть (β_{Y,X}).hom = (β_{X,Y}).inv.

LaTeX

$$$ (\\beta_{Y X}).hom = (\\beta_{X Y}).inv $$$

Lean4

theorem braiding_swap_eq_inv_braiding {C : Type u₁} [Category.{v₁} C] [MonoidalCategory C] [SymmetricCategory C]
    (X Y : C) : (β_ Y X).hom = (β_ X Y).inv :=
  Iso.inv_ext' (symmetry X Y)

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