English
The morphism hom is a canonical map from mappingCone g to mappingCone of the triangle f,g, yielding a homotopy equivalence.
Русский
Морфизм hom — каноническое отображение от mappingCone g к mappingCone треугольника, образующего гомотопическую эквивалентность.
LaTeX
$$$\text{hom } f\, g : \operatorname{mappingCone} g \to \operatorname{mappingCone}(\operatorname{mappingConeCompTriangle}(f,g).mor_1$$$
Lean4
/-- Given two composable morphisms `f` and `g` in the category of cochain complexes, this
is the canonical morphism (which is an homotopy equivalence) from `mappingCone g` to
the mapping cone of the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`. -/
noncomputable def hom : mappingCone g ⟶ mappingCone (mappingConeCompTriangle f g).mor₁ :=
lift _ (descCocycle g (Cochain.ofHom (inr f)) 0 (zero_add 1) (by simp))
(descCochain _ 0 (Cochain.ofHom (inr (f ≫ g))) (neg_add_cancel 1))
(by
ext p _ rfl
dsimp [mappingConeCompTriangle, map]
simp [ext_from_iff _ _ _ rfl, inl_v_d_assoc _ (p + 1) p (p + 2) (by cutsat) (by cutsat)])
