English
The differential respects composition via a Leibniz-type rule: δ(n1+n2) (z1 ∘ z2) = z1 ∘ δ(n2,m2)(z2) + (-1)^{n2} (δ(n1,m1)(z1)) ∘ z2.
Русский
Дифференциал в отношении композиции выполняется согласно закону Лейбница: δ(z1 ∘ z2) = z1 ∘ δ(z2) + (-1)^{deg(z2)} δ(z1) ∘ z2.
LaTeX
$$$δ_{n_1+n_2, m} (z_1 \\circ z_2) = z_1 \\circ δ_{n_2,m_2} (z_2) + n_2^{(-1)} (δ_{n_1,m_1}(z_1)) \\circ z_2.$$$
Lean4
theorem δ_v (hnm : n + 1 = m) (z : Cochain F G n) (p q : ℤ) (hpq : p + m = q) (q₁ q₂ : ℤ) (hq₁ : q₁ = q - 1)
(hq₂ : p + 1 = q₂) :
(δ n m z).v p q hpq =
z.v p q₁ (by rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]) ≫ G.d q₁ q +
m.negOnePow • F.d p q₂ ≫ z.v q₂ q (by rw [← hq₂, add_assoc, add_comm 1, hnm, hpq]) :=
by
obtain rfl : q₁ = p + n := by cutsat
obtain rfl : q₂ = p + m - n := by cutsat
rfl
