English
For any −1-degree cochain z, the differential δ_{−1,0} z is equal to the cochain ofHom of the Homotopy-null-homotopic map applied to z in an adjusted form: δ_{−1,0} z = Cochain.ofHom(Homotopy.nullHomotopicMap'( ... z ... )).
Русский
Для коцепона степени −1: δ_{−1,0} z равно коцепе ofHom применённому к гомотопии nullHomotopicMap' на z с соответствующим преобразованием.
LaTeX
$$$\delta_{-1\,0} z = \operatorname{Cochain.ofHom}(\operatorname{Homotopy.nullHomotopicMap}'(f(z)))$$$
Lean4
theorem δ_neg_one_cochain (z : Cochain F G (-1)) :
δ (-1) 0 z =
Cochain.ofHom
(Homotopy.nullHomotopicMap' (fun i j hij => z.v i j (by dsimp at hij; rw [← hij, add_neg_cancel_right]))) :=
by
ext p
rw [δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]
simp only [one_smul, Cochain.ofHom_v, Int.negOnePow_zero]
rw [Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)
(show (ComplexShape.up ℤ).Rel p (p + 1) by simp)]
abel
