isEquivalence

Mathlib.CategoryTheory.Sums.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sum.Swap.isEquivalence

English

The swap operation defines an equivalence of categories between C ⊕ D and D ⊕ C.

Русский

Операция обмена определяет эквивалентность категорий между C ⊕ D и D ⊕ C.

LaTeX

$$$(C \oplus D) \simeq (D \oplus C)$$$

Lean4

instance isEquivalence : (swap C D).IsEquivalence :=
  (by infer_instance : (equivalence C D).functor.IsEquivalence)

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

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

Разделы

Аффилиация

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