equivalenceCounitIso

Mathlib.AlgebraicTopology.DoldKan.Compatibility

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso

Lean4

/-- The counit isomorphism of `equivalence`. -/
@[simps!]
def equivalenceCounitIso : G ⋙ F ⋙ eB.inverse ≅ 𝟭 B :=
  calc
    G ⋙ F ⋙ eB.inverse ≅ (G ⋙ F) ⋙ eB.inverse := (associator _ _ _).symm
    _ ≅ eB.functor ⋙ eB.inverse := (isoWhiskerRight η _)
    _ ≅ 𝟭 B := eB.unitIso.symm

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

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

Разделы

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

Аффилиация

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