English
There is a natural equivalence between the set of homotopies from f to g and the set of homotopies from f − g to 0. Concretely, f is homotopic to g if and only if f − g is homotopic to the zero morphism.
Русский
Существует естественное эквивалентное соответствие между гомотопиями от f к g и гомотопиями от f − g к нулю. Ровно: f гомотопически эквивалентен g тогда и только тогда, когда f − g гомотопичен к нулю.
LaTeX
$$$\text{Homotopy}(f,g) \cong \text{Homotopy}(f-g,0).$$$
Lean4
/-- `f` is homotopic to `g` iff `f - g` is homotopic to `0`.
-/
def equivSubZero : Homotopy f g ≃ Homotopy (f - g) 0
where
toFun
h :=
{ hom := fun i j => h.hom i j
zero := fun _ _ w => h.zero _ _ w
comm := fun i => by simp [h.comm] }
invFun
h :=
{ hom := fun i j => h.hom i j
zero := fun _ _ w => h.zero _ _ w
comm := fun i => by simpa [sub_eq_iff_eq_add] using h.comm i }
left_inv := by cat_disch
right_inv := by cat_disch
