English
In the simplified inductive constructor mk', the 0-th component equals the given X0: (mk' X0 X1 d).X 0 = X0.
Русский
В упрощенном конструкторе mk' нулевой компонент равен заданному X0.
LaTeX
$$$$(\\mathrm{mk}'\\ X_0 X_1\ d).X_0 = X_0$$$$
Lean4
/-- A simpler inductive constructor for `ℕ`-indexed chain complexes.
You provide explicitly the first differential,
then a function which takes a differential,
and returns the next object, its differential, and the fact it composes appropriately to zero.
-/
def mk' (X₀ X₁ : V) (d : X₁ ⟶ X₀) (succ' : ∀ {X₀ X₁ : V} (f : X₁ ⟶ X₀), Σ' (X₂ : V) (d : X₂ ⟶ X₁), d ≫ f = 0) :
ChainComplex V ℕ :=
mk _ _ _ _ _ (succ' d).2.2 (fun S => succ' S.f)
