English
There is a coinductive construction yielding a homotopy between a given degreewise morphism of cochain complexes and the zero map, built by a recursive, guarded specification of components and a proof that the homotopy equations hold.
Русский
Существует коиндуктивная конструкция гомотопии между заданным отображением между коцепохемиями и нулевым отображением, строимая по рекурсивному, охраняемому описанию компонент и доказательству выполнения гомотопийных уравнений.
LaTeX
$$$\\text{There exists a family } h_i : P_i \\to Q_{i+1} \\text{ satisfying the homotopy relations } e.f(i+1) = P.d(i+1,i)\\, h_i + h_{i+1} \\, Q.d(i+2,i+1).$$$
Lean4
/-- An auxiliary construction for `mkCoinductive`.
Here we build by induction a family of diagrams,
but don't require at the type level that these successive diagrams actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy)
in `mkCoinductive`.
At this stage, we don't check the homotopy condition in degree 0,
because it "falls off the end", and is easier to treat using `xNext` and `xPrev`,
which we do in `mkInductiveAux₂`.
-/
@[simp]
def mkCoinductiveAux₁ :
∀ n,
Σ' (f : P.X (n + 1) ⟶ Q.X n) (f' : P.X (n + 2) ⟶ Q.X (n + 1)),
e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f'
| 0 => ⟨zero, one, comm_one⟩
| 1 => ⟨one, (succ 0 ⟨zero, one, comm_one⟩).1, (succ 0 ⟨zero, one, comm_one⟩).2⟩
| n + 2 =>
⟨(mkCoinductiveAux₁ (n + 1)).2.1, (succ (n + 1) (mkCoinductiveAux₁ (n + 1))).1,
(succ (n + 1) (mkCoinductiveAux₁ (n + 1))).2⟩
