equivalence

Mathlib.AlgebraicTopology.DoldKan.Compatibility

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

Lean4

/-- The equivalence `A ≅ B` whose functor is `F ⋙ eB.inverse` and
whose inverse is `G : B ≅ A`. -/
@[simps! inverse]
def equivalence : A ≌ B :=
  ((equivalence₂ eB hF).changeInverse
    (calc
      eB.functor ⋙ e'.inverse ⋙ eA.inverse ≅ (eB.functor ⋙ e'.inverse) ⋙ eA.inverse := (associator _ _ _).symm
      _ ≅ (G ⋙ eA.functor) ⋙ eA.inverse := (isoWhiskerRight hG _)
      _ ≅ G ⋙ eA.functor ⋙ eA.inverse := (associator _ _ _)
      _ ≅ G ⋙ 𝟭 A := (isoWhiskerLeft _ eA.unitIso.symm)
      _ ≅ G := G.rightUnitor))

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

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

Разделы

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

Аффилиация

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