English
Let z1 be a 0-cochain from F to G and z2 a cochain in degree n2 from G to K, with integers m2 and h2 = n2 + 1. Then applying the differential δ at (n2, m2) to the composite z1 ∘ z2 (shifted by n2) equals the composite of z1 with δ on z2 (shifted by m2) plus (−1)^{n2} times the composite of δ on z1 (shifted by 0→1) with z2, adjusted by the same shift on the second factor. In symbols, δ_{n2,m2}(z1 ∘ z2) = z1 ∘ δ_{n2,m2}(z2) + (−1)^{n2} (δ_{0,1} z1) ∘ z2, up to the degree shifts.
Русский
Пусть z1 — 0‑коцеп (коцепта между F и G), z2 — коцептан между G и K в степени n2, и пусть m2 = n2 + 1. Тогда дифференциал δ применяется к композиции z1 ∘ z2 (сдвинутой на n2) и равен композиции z1 с δ(z2) (сдвинутой на m2) плюс (-1)^{n2} раз сумма δ(z1)∘ z2 с соответствующим сдвигом по степеням. Формула: δ_{n2,m2}(z1 ∘ z2) = z1 ∘ δ_{n2,m2}(z2) + n2.negOnePow · (δ_{0,1} z1) ∘ z2.
LaTeX
$$$\delta_{n_2,m_2}(z_1 \circ z_2 (\operatorname{zero\_add} n_2)) = z_1 \circ (\delta_{n_2,m_2} z_2)(\operatorname{zero\_add} m_2) + n_2.negOnePow \cdot ((\delta 0 1 z_1).\text{comp} z_2 (by rw [add_comm, h_2]))$$$
Lean4
theorem δ_zero_cochain_comp {n₂ : ℤ} (z₁ : Cochain F G 0) (z₂ : Cochain G K n₂) (m₂ : ℤ) (h₂ : n₂ + 1 = m₂) :
δ n₂ m₂ (z₁.comp z₂ (zero_add n₂)) =
z₁.comp (δ n₂ m₂ z₂) (zero_add m₂) + n₂.negOnePow • ((δ 0 1 z₁).comp z₂ (by rw [add_comm, h₂])) :=
δ_comp z₁ z₂ (zero_add n₂) 1 m₂ m₂ h₂ (zero_add 1) h₂
