English
As above, with roles swapped: δ_{n1,m1}(z1 ∘ z2 (add_zero n1)) equals z1 ∘ (δ_{0,1} z2) h1 plus (δ_{n1,m1} z1) ∘ z2.
Русский
Аналогично, при перестановке ролей: δ_{n1,m1}(z1 ∘ z2 (add_zero n1)) = z1 ∘ (δ_{0,1} z2) h1 + (δ_{n1,m1} z1) ∘ z2.
LaTeX
$$$\\delta_{n_1,m_1}(z_1 \\circ z_2 (\\operatorname{add\\_zero} n_1)) = z_1 \\circ (\\delta_{0,1} z_2)\\, h_1 + (\\delta_{n_1,m_1} z_1) \\circ z_2$$$
Lean4
@[simp]
theorem δ_ofHomotopy {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) :
δ (-1) 0 (Cochain.ofHomotopy h) = Cochain.ofHom φ₁ - Cochain.ofHom φ₂ :=
by
ext p
have eq := h.comm p
rw [dNext_eq h.hom (show (ComplexShape.up ℤ).Rel p (p + 1) by simp),
prevD_eq h.hom (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)] at eq
rw [Cochain.ofHomotopy, δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]
simp only [Cochain.mk_v, one_smul, Int.negOnePow_zero, Cochain.sub_v, Cochain.ofHom_v, eq]
abel
