υ

Mathlib.AlgebraicTopology.DoldKan.Compatibility

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

Lean4

/-- The isomorphism `eA.functor ≅ F ⋙ e'.inverse` deduced from the
unit isomorphism of `e'` and the isomorphism `hF : eA.functor ⋙ e'.functor ≅ F`. -/
@[simps!]
def υ : eA.functor ≅ F ⋙ e'.inverse :=
  calc
    eA.functor ≅ eA.functor ⋙ 𝟭 A' := (rightUnitor _).symm
    _ ≅ eA.functor ⋙ e'.functor ⋙ e'.inverse := (isoWhiskerLeft _ e'.unitIso)
    _ ≅ (eA.functor ⋙ e'.functor) ⋙ e'.inverse := (associator _ _ _).symm
    _ ≅ F ⋙ e'.inverse := isoWhiskerRight hF _

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

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

Разделы

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

Аффилиация

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