equivalence_unitIso

Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

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

English

The unitIso of the equivalence equals ε.

Русский

Единичное изоморфление эквивалентности равно ε.

LaTeX

$$$$ \\text{equivalence.unitIso} = \\varepsilon. $$$$

Lean4

theorem equivalence_unitIso : DoldKan.equivalence.unitIso = (ε : 𝟭 (SimplicialObject C) ≅ N ⋙ Γ) :=
  Compatibility.equivalenceUnitIso_eq hε

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

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

Разделы

Аффилиация

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