nullHomotopicMap

Mathlib.Algebra.Homology.HomotopyCofiber

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

Lean4

/-- A null homotopic map `K.cylinder ⟶ K.cylinder` which identifies to
`π K ≫ ι₀ K - 𝟙 _`, see `nullHomotopicMap_eq`. -/
noncomputable def nullHomotopicMap : K.cylinder ⟶ K.cylinder :=
  Homotopy.nullHomotopicMap'
    (fun i j hij => homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ (biprod.snd : K ⊞ K ⟶ K).f i ≫ inlX K i j hij)

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

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

Разделы

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

Аффилиация

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