compRight

Mathlib.Algebra.Homology.Homotopy

URI: https://scilib.ai/kg/mathlib#Homotopy.compRight

Lean4

/-- homotopy is closed under composition (on the right) -/
@[simps]
def compRight {e f : C ⟶ D} (h : Homotopy e f) (g : D ⟶ E) : Homotopy (e ≫ g) (f ≫ g)
    where
  hom i j := h.hom i j ≫ g.f j
  zero i j w := by rw [h.zero i j w, zero_comp]
  comm
    i := by
    rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp, comp_f, Preadditive.add_comp]

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

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

Разделы

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

Аффилиация

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