English
In the inductive construction mk of ChainComplex, the 0-th component equals the given object X0: (mk X0 X1 X2 d0 d1 s succ).X 0 = X0.
Русский
При конструировании mk цепного комплекса нулевой компонент равен заданному объекту X0.
LaTeX
$$$$(\\mathrm{mk}\\ X_0 X_1 X_2\ \ d_0\ d_1\ s\ succ).X_0 = X_0$$$$
Lean4
/-- An inductive constructor for `ℕ`-indexed chain complexes.
You provide explicitly the first two differentials,
then a function which takes two differentials and the fact they compose to zero,
and returns the next object, its differential, and the fact it composes appropriately to zero.
See also `mk'`, which only sees the previous differential in the inductive step.
-/
def mk : ChainComplex V ℕ :=
of (fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₃) (fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).g) fun n =>
(mkAux X₀ X₁ X₂ d₀ d₁ s succ n).zero
