English
Let z1 be a F→G cochain of degree n1 and z2 be a G→K cochain of degree 0, with m1 = n1+1. Then δ_{n1,m1} applied to the composition z1 ∘ z2 (shifted by n1) equals the composition of z1 with δ on z2 (shifted by h1) plus the composition of δ on z1 (shifted by 0) with z2.
Русский
Пусть z1: F→G в степени n1 и z2: G→K в степени 0, и пусть m1 = n1+1. Тогда δ_{n1,m1}(z1 ∘ z2 (добавление 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 (\operatorname{add\_zero} m_1)$$$
Lean4
theorem δ_comp_zero_cochain {n₁ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K 0) (m₁ : ℤ) (h₁ : n₁ + 1 = m₁) :
δ n₁ m₁ (z₁.comp z₂ (add_zero n₁)) = z₁.comp (δ 0 1 z₂) h₁ + (δ n₁ m₁ z₁).comp z₂ (add_zero m₁) := by
simp only [δ_comp z₁ z₂ (add_zero n₁) m₁ 1 m₁ h₁ h₁ (zero_add 1), one_smul, Int.negOnePow_zero]
