descHomotopyZeroSucc — Mathlib

English

Definition: Given f and n and morphisms g, g' with a relation w between f and g,g', define the (n+3)-th component descent using the exact succ piece.

Русский

Определение: для данного f, n и морфизмов g,g' с условием w между ними, задаётся спуск в степени n+3 через точность succ.

LaTeX

$$descHomotopyZeroSucc(f, n, g, g', w) = (I.exact_succ (n+1)).descToInjective (f.f (n+2) - g' ≫ J.cocomplex.d _ _ )$$

Lean4

/-- An auxiliary definition for `descHomotopyZero`. -/
def 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.X (n + 3) ⟶ J.cocomplex.X (n + 2) :=
  (I.exact_succ (n + 1)).descToInjective (f.f (n + 2) - g' ≫ J.cocomplex.d _ _)
    (by
      dsimp
      rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp, Category.assoc, Category.assoc,
        HomologicalComplex.d_comp_d, comp_zero, add_zero, sub_self])

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