swapIsEquivalence

Mathlib.CategoryTheory.Products.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Prod.swapIsEquivalence

English

The swap functor is an equivalence of categories: swap C D : C × D ≌ D × C.

Русский

Функтор обмена является эквивалентностью категорий: swap C D : C × D ≌ D × C.

LaTeX

$$$\mathrm{swap}: C \times D \xrightarrow{\sim} D \times C$ is an equivalence$$

Lean4

instance swapIsEquivalence : (swap C D).IsEquivalence :=
  (by infer_instance : (braiding C D).functor.IsEquivalence)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru