comp_descHomotopyZeroOne — Mathlib

English

Compatibility of the next descent with the differential: I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm = f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1.

Русский

Совместимость следующего спуска с дифференциалом: I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm = f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1.

LaTeX

$$I.cocomplex.d 1 2 \; ≫ \; \mathrm{descHomotopyZeroOne}(f, comm) = f.f 1 - \mathrm{descHomotopyZeroZero}(f, comm) ≫ J.cocomplex.d 0 1$$

Lean4

@[reassoc (attr := simp)]
theorem comp_descHomotopyZeroOne {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z}
    (f : I.cocomplex ⟶ J.cocomplex) (comm : I.ι ≫ f = (0 : _ ⟶ J.cocomplex)) :
    I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm = f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 :=
  (I.exact_succ 0).comp_descToInjective _ _

Похожие утверждения