braiding — Mathlib

English

There is a natural equivalence between C × D and D × C given by the swap functor.

Русский

Существуют естественные эквиваленсы между C × D и D × C, задаваемые функтором обмена.

LaTeX

$$$\mathrm{braiding}: C \times D \simeq D \times C$ with \mathrm{swap} as the underlying functor$$

Lean4

/-- The equivalence, given by swapping factors, between `C × D` and `D × C`.
-/
@[simps]
def braiding : C × D ≌ D × C where
  functor := swap C D
  inverse := swap D C
  unitIso := Iso.refl _
  counitIso := Iso.refl _

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