English
The composition hom f g ≫ inv f g is the identity on the mappingCone g; i.e., the pair (hom, inv) forms a homotopy equivalence.
Русский
Составление hom f g затем inv f g даёт тождественности на mappingCone g; пары образуют гомотопическую эквивалентность.
LaTeX
$$$\text{hom } f\, g \;\circ\; \text{inv } f\, g = \mathrm{id}_{\operatorname{mappingCone} g}$$$
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 the mapping cone of
the morphism `mappingCone f ⟶ mappingCone (f ≫ g)` to `mappingCone g`. -/
noncomputable def inv : mappingCone (mappingConeCompTriangle f g).mor₁ ⟶ mappingCone g :=
desc _ ((snd f).comp (inl g) (zero_add (-1)))
(desc _ ((Cochain.ofHom f).comp (inl g) (zero_add (-1))) (inr g) (by simp))
(by
ext p
rw [ext_from_iff _ (p + 1) _ rfl, ext_to_iff _ _ (p + 1) rfl]
simp [map, δ_zero_cochain_comp, Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p (by cutsat) (by cutsat)])
