English
For composable f and g, there is a homotopy equivalence between the cone of g and the cone of the morphism mappingCone f → mappingCone(f ≫ g).mor1. This exhibits a fundamental relation between successive mapping cones.
Русский
Для сопряжённых f и g существует гомотопическая эквивалентность между конусом g и конусом морфизма mappingCone f → mappingCone(f ≫ g).mor1, демонстрирующая ключевую связь между последовательными конусами отображений.
LaTeX
$$$\mathrm{HomotopyEquiv}(\mathrm{mappingCone}(g), \mathrm{mappingCone}(\mathrm{mappingConeCompTriangle}(f,g).mor_1))$$$
Lean4
/-- Given two composable morphisms `f` and `g` in the category of cochain complexes,
this is the homotopy equivalence `mappingConeCompHomotopyEquiv f g`
between `mappingCone g` and the mapping cone of
the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`. -/
noncomputable def mappingConeCompHomotopyEquiv :
HomotopyEquiv (mappingCone g) (mappingCone (mappingConeCompTriangle f g).mor₁)
where
hom := MappingConeCompHomotopyEquiv.hom f g
inv := MappingConeCompHomotopyEquiv.inv f g
homotopyHomInvId := Homotopy.ofEq (by simp)
homotopyInvHomId := MappingConeCompHomotopyEquiv.homotopyInvHomId f g
