English
The full coinductive construction assembling a homotopy e 0 between chain maps in the cochain setting, using the previous auxiliary steps mkCoinductiveAux₁ and mkCoinductiveAux₂ to define all components and verify the homotopy equations.
Русский
Полная коиндективная конструкция, собирающая гомотопию e 0 между цепными отображениями в коцепном контексте, используя предыдущие вспомогательные шаги mkCoinductiveAux₁ и mkCoinductiveAux₂ для определения всех компонент и проверки гомотопийных уравнений.
LaTeX
$$There exists a family {h_i} giving a homotopy e 0 with components built from mkCoinductiveAux₁ and mkCoinductiveAux₂ satisfying the homotopy equations.$$
Lean4
/-- A constructor for a `Homotopy e 0`, for `e` a chain map between `ℕ`-indexed cochain 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 mkCoinductive : Homotopy e 0
where
hom i
j := if h : j + 1 = i then (P.xNextIso h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).2.1 else 0
zero i j w := by rw [dif_neg]; exact w
comm
i := by
dsimp
simp only [add_zero]
rw [add_comm]
refine (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans ?_
congr
· cases i
· dsimp [toPrev, mkCoinductiveAux₂]
· dsimp [toPrev]
simp only [CochainComplex.prev_nat_succ, dite_true]
rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]
dsimp [xPrevIso]
rw [comp_id]
· dsimp [fromNext]
rw [dif_pos (by simp only [CochainComplex.next])]
simp [xNextIso, id_comp]
