symmetry — Mathlib

English

In a symmetric monoidal category, the braiding is an involution in the sense that composing the braiding with its opposite returns the identity on the tensor product: β_{X,Y} ∘ β_{Y,X} = id_{X⊗Y}.

Русский

В симметричной моноидальной категории композиция браидинга с обратным браидингом даёт тождество на тензорном произведении: β_{X,Y} ∘ β_{Y,X} = id_{X⊗Y}.

LaTeX

$$$ (\mathrm{braiding}(X,Y)^{\mathrm{hom}}) \circ (\mathrm{braiding}(Y,X)^{\mathrm{hom}}) = \mathrm{Id}_{X \otimes Y} $$$

Lean4

@[reassoc (attr := simp)]
theorem symmetry [SymmetricCategory C] [HasTensor X Y] [HasTensor Y X] :
    (braiding X Y).hom ≫ (braiding Y X).hom = 𝟙 _ :=
  by
  dsimp [braiding]
  cat_disch

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