mapHomotopy

Mathlib.Algebra.Homology.Homotopy

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.mapHomotopy

Lean4

/-- An additive functor takes homotopies to homotopies. -/
@[simps]
def mapHomotopy (F : V ⥤ W) [F.Additive] {f g : C ⟶ D} (h : Homotopy f g) :
    Homotopy ((F.mapHomologicalComplex c).map f) ((F.mapHomologicalComplex c).map g)
    where
  hom i j := F.map (h.hom i j)
  zero i j w := by dsimp; rw [h.zero i j w, F.map_zero]
  comm
    i := by
    have H := h.comm i
    dsimp [dNext, prevD] at H ⊢
    simp [H]

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

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

Разделы

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

Аффилиация

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