English
There exists a constructive way to build a homotopy between a chain map e : P → Q and the zero map, by an inductive procedure that specifies the initial components (in degrees 0 and 1) and then recursively determines each successive component using a prescribed homotopy condition.
Русский
Существует конструктивное построение гомотопии между цепным отображением e : P → Q и нулевым отображением, задаваемое индуктивной процедурой: в степенях 0 и 1 заданы начальные компоненты, затем для каждого следующего компонента определяется по заданному условию гомотопии.
LaTeX
$$$\\exists \\{h_i : P_X{i} \\to Q_X{i+1}\\}_{i \\in \\mathbb{N}} \\text{ such that } e.f(i+1) = P.d(i+1,i) \\circ h_i + h_{i+1} \\circ Q.d(i+2,i+1).$$$
Lean4
/-- A constructor for a `Homotopy e 0`, for `e` a chain map between `ℕ`-indexed chain complexes,
working by induction.
You need to provide the components of the homotopy in degrees 0 and 1,
show that these satisfy the homotopy condition,
and then give a construction of each component,
and the fact that it satisfies the homotopy condition,
using as an inductive hypothesis the data and homotopy condition for the previous two components.
-/
def mkInductive : Homotopy e 0
where
hom i
j := if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).2.1 ≫ (Q.xPrevIso h).hom else 0
zero i j w := by rw [dif_neg]; exact w
comm
i := by
dsimp
simp only [add_zero]
refine (mkInductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans ?_
congr
· cases i
· dsimp [fromNext, mkInductiveAux₂]
· dsimp [fromNext]
simp only [ChainComplex.next_nat_succ, dite_true]
rw [mkInductiveAux₃ e zero comm_zero one comm_one succ]
dsimp [xNextIso]
rw [id_comp]
· dsimp [toPrev]
rw [dif_pos (by simp only [ChainComplex.prev])]
simp [xPrevIso, comp_id]
