homotopyCofiber — Mathlib

Lean4
/-- The homotopy cofiber of a morphism of homological complexes,
also known as the mapping cone. -/
@[simps]
noncomputable def homotopyCofiber : HomologicalComplex C c
    where
  X i := homotopyCofiber.X φ i
  d i j := homotopyCofiber.d φ i j
  shape i j hij := homotopyCofiber.shape φ i j hij
  d_comp_d' i j k hij
    hjk := by
    apply homotopyCofiber.ext_from_X φ j i hij
    · dsimp
      simp only [comp_zero, homotopyCofiber.inlX_d_assoc φ i j k hij hjk, add_comp, assoc, homotopyCofiber.inrX_d,
        Hom.comm_assoc, neg_comp]
      by_cases hk : c.Rel k (c.next k)
      · simp [homotopyCofiber.inlX_d φ j k _ hjk hk]
      · simp [homotopyCofiber.inlX_d' φ j k hjk hk]
    · simp
Похожие утверждения