English
Definition: For Y, Z with injective resolutions I, J and a cocomplex morphism f, together with a null-homotopy condition comm, the auxiliary morphism descHomotopyZeroZero: I.cocomplex.X1 → J.cocomplex.X0 is defined by exactness data.
Русский
Определение: для Y, Z и резолюций I, J, а также морфизма кокомлекс f и условия comm, задаётся вспомогательный морфизм descHomotopyZeroZero: I.cocomplex.X1 → J.cocomplex.X0, определяемый данными точности.
LaTeX
$$descHomotopyZeroZero(f, comm) = I.exact₀.descToInjective (f.f 0) (congr_fun (congr_arg HomologicalComplex.Hom.f comm) 0)$$
Lean4
/-- An auxiliary definition for `descHomotopyZero`. -/
def descHomotopyZeroZero {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z}
(f : I.cocomplex ⟶ J.cocomplex) (comm : I.ι ≫ f = 0) : I.cocomplex.X 1 ⟶ J.cocomplex.X 0 :=
I.exact₀.descToInjective (f.f 0) (congr_fun (congr_arg HomologicalComplex.Hom.f comm) 0)
