English
There exists a unique lift g'' making the higher differential commute in the successor step of the descent construction between injective resolutions.
Русский
Существование единственного подъема g'' обеспечивающего commute на следующем шаге схемы спуска между разрешениями.
LaTeX
$$\(\exists! g'' : J.cocomplex.X (n+2) \to I.cocomplex.X (n+2) \;\text{with appropriate compatibility}\)$$
Lean4
/-- Auxiliary construction for `desc`. -/
def descFSucc {Y Z : C} (I : InjectiveResolution Y) (J : InjectiveResolution Z) (n : ℕ)
(g : J.cocomplex.X n ⟶ I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1))
(w : J.cocomplex.d n (n + 1) ≫ g' = g ≫ I.cocomplex.d n (n + 1)) :
Σ' g'' : J.cocomplex.X (n + 2) ⟶ I.cocomplex.X (n + 2),
J.cocomplex.d (n + 1) (n + 2) ≫ g'' = g' ≫ I.cocomplex.d (n + 1) (n + 2) :=
⟨(J.exact_succ n).descToInjective (g' ≫ I.cocomplex.d (n + 1) (n + 2)) (by simp [reassoc_of% w]),
(J.exact_succ n).comp_descToInjective _ _⟩
