English
Definition: For Y,Z with I,J, and a morphism f of cocomplexes with commutator, define descHomotopyZeroOne to be the next degree descent using the exact succ piece and compatibility with differentials.
Русский
Определение: для Y, Z с резолюциями I,J и морфизмом кокомлексa f с сопряжениями, задаётся descend в степени 2 через точность succ и совместимость дифференциалов.
LaTeX
$$descHomotopyZeroOne(f, comm) = (I.exact_succ 0).descToInjective (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) (proof-compatibility)$$
Lean4
/-- An auxiliary definition for `descHomotopyZero`. -/
def descHomotopyZeroOne {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z}
(f : I.cocomplex ⟶ J.cocomplex) (comm : I.ι ≫ f = (0 : _ ⟶ J.cocomplex)) : I.cocomplex.X 2 ⟶ J.cocomplex.X 1 :=
(I.exact_succ 0).descToInjective (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1)
(by rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm, HomologicalComplex.Hom.comm, sub_self])
