equivalence_inverse

Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.DoldKan.equivalence_inverse

English

The inverse of the Dold-Kan equivalence is Γ.

Русский

Обратная к эквивалентности Дольда-Кана равна Γ.

LaTeX

$$$$ \\text{equivalence}^{-1} = \\Gamma. $$$$

Lean4

theorem equivalence_inverse : (equivalence : SimplicialObject C ≌ _).inverse = Γ :=
  rfl

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

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

Разделы

Аффилиация

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