πCompι₀Homotopy

Mathlib.Algebra.Homology.HomotopyCofiber

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.cylinder.πCompι₀Homotopy

Lean4

/-- The homotopy between `π K ≫ ι₀ K` and `𝟙 K.cylinder`. -/
noncomputable def πCompι₀Homotopy : Homotopy (π K ≫ ι₀ K) (𝟙 K.cylinder) :=
  Homotopy.equivSubZero.symm
    ((Homotopy.ofEq (πCompι₀Homotopy.nullHomotopicMap_eq K hc).symm).trans (πCompι₀Homotopy.nullHomotopy K))

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

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

Разделы

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

Аффилиация

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