English
Compatibility of the composition of desc with successive descents: the differential at n+2 composed with the succ descent equals f at n+2 minus g' composed with a differential.
Русский
Совместимость композиции desc с последовательными спусками: d_{n+2,n+3} ∘ descHomotopyZeroSucc = f.f_{n+2} - g' ∘ d_{n+1,n+2}.
LaTeX
$$I.cocomplex.d (n+2) (n+3) ≫ \mathrm{descHomotopyZeroSucc}(f, n, g, g', w) = f.f (n+2) - g' ≫ J.cocomplex.d _ _$$
Lean4
@[reassoc (attr := simp)]
theorem comp_descHomotopyZeroSucc {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z}
(f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n)
(g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1))
(w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) :
I.cocomplex.d (n + 2) (n + 3) ≫ descHomotopyZeroSucc f n g g' w = f.f (n + 2) - g' ≫ J.cocomplex.d _ _ :=
(I.exact_succ (n + 1)).comp_descToInjective _ _
