symmetry

Mathlib.CategoryTheory.Sums.Basic

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

← MathLib Explorer

English

The double swap is naturally isomorphic to the identity functor on C ⊕ D.

Русский

Двойной обмен естественным образом изоморфна тождественному функтору на C ⊕ D.

LaTeX

$$swap(C,D) ∘ swap(D,C) ≅ 1_{C ⊕ D}$$

Lean4

/-- The double swap on `C ⊕ D` is naturally isomorphic to the identity functor. -/
def symmetry : swap C D ⋙ swap D C ≅ 𝟭 (C ⊕ D) :=
  (equivalence C D).unitIso.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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