English
There exists an ℕ-indexed cochain complex built inductively from X0, X1, X2 with differentials d0, d1 and a step-succ function: mk : CochainComplex V ℕ is defined so that its nth component is the X1-part of mkAux(n), its nth differential is mkAux(n).f, and the nth zero-claim is mkAux(n).zero.
Русский
Существует чрез индукцию коогранный комплекс с индексацией по ℕ, строимый из X0, X1, X2 и дифференциалов d0, d1; на шаге задаётся succ. Определим mk: CochainComplex V ℕ так, что его n-й компонент равен X1-компоненте mkAux(n), соответствующий дифференциал равен mkAux(n).f, и нулевая тождественная часть равна mkAux(n).zero.
LaTeX
$$$\\mathrm{mk} : \\mathrm{CochainComplex}\; V\\; \\mathbb{N}\\;\\text{ with }\\; \\mathrm{mk}_n = (\\mathrm{mkAux}(X_0,X_1,X_2,d_0,d_1,succ,n)).\\mathrm{X}_1, \\; \\mathrm{mk}\\.d_n = (\\mathrm{mkAux}(X_0,X_1,X_2,d_0,d_1,succ,n)).\\mathrm{f}, \\; \\mathrm{mk}\\.zero = (\\mathrm{mkAux}(X_0,X_1,X_2,d_0,d_1,succ,n)).\\mathrm{zero}.$$
Lean4
/-- An inductive constructor for `ℕ`-indexed cochain 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 : CochainComplex 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).f) fun n =>
(mkAux X₀ X₁ X₂ d₀ d₁ s succ n).zero
