English
For the simplified constructor mk', the degree-0 term equals X0.
Русский
Для упрощённого конструктора mk' нулевой член равен X0.
LaTeX
$$$\\big(\\mathrm{mk}'\\; X_0 X_1 d_0 succ'\\big).X_0 = X_0$$$
Lean4
/-- A simpler inductive constructor for `ℕ`-indexed cochain 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, X₀ ⟶ X₁, Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0) :
(succ' : ∀ {X₀ X₁ : V} (f : X₀ ⟶ X₁), Σ' (X₂ : V) (d : X₁ ⟶ X₂), f ≫ d = 0) : CochainComplex V ℕ :=
mk _ _ _ _ _ (succ' d).2.2 (fun S => succ' S.g)
