equivalence_counitIso

Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

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

English

The inverse of the equivalence is Γ (reiterated).

Русский

Обратная эквивалентности повторно равна Γ.

LaTeX

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

Lean4

theorem equivalence_counitIso : DoldKan.equivalence.counitIso = (η : Γ ⋙ N ≅ 𝟭 (ChainComplex C ℕ)) :=
  Compatibility.equivalenceCounitIso_eq hη

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

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

Разделы

Аффилиация

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