English
Definition: The descent of zero morphism f: I.cocomplex ⟶ J.cocomplex is homotopic to zero via a coinductive construction using Zero, One, and a recursion over n with descHomotopyZeroZero, descHomotopyZeroOne, and descHomotopyZeroSucc.
Русский
Определение: спуск нулевого морфизма f является гомотопией к нулю через коиндуктивное построение, используя descHomotopyZeroZero, descHomotopyZeroOne и descHomotopyZeroSucc.
LaTeX
$$descHomotopy(f, comm) = Homotopy.mkCoinductive _ (descHomotopyZeroZero f comm) (descHomotopyZeroOne f comm) (descHomotopyZeroSucc f ...)$$
Lean4
/-- Any descent of the zero morphism is homotopic to zero. -/
def descHomotopyZero {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
(comm : I.ι ≫ f = 0) : Homotopy f 0 :=
Homotopy.mkCoinductive _ (descHomotopyZeroZero f comm) (by simp) (descHomotopyZeroOne f comm) (by simp)
(fun n ⟨g, g', w⟩ => ⟨descHomotopyZeroSucc f n g g' (by simp only [w, add_comm]), by simp⟩)
