English
A generalized Leibniz rule for δ on compositions in two-stage indices, connecting δ on z1 and z2 via multiple degree shifts (long formula given).
Русский
Обобщённое правило Лейбница для δ на композиции в двух степенях, связывающее δ на z1 и z2 через несколько сдвигов степеней (см. детальное выражение).
LaTeX
$$$δ(n_1+n_2, m_1+n_2)(z_1 \\circ z_2) = z_1 \\circ δ(n_2, m_2)(z_2) + ...$$$
Lean4
theorem δ_comp {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (m₁ m₂ m₁₂ : ℤ)
(h₁₂ : n₁₂ + 1 = m₁₂) (h₁ : n₁ + 1 = m₁) (h₂ : n₂ + 1 = m₂) :
δ n₁₂ m₁₂ (z₁.comp z₂ h) =
z₁.comp (δ n₂ m₂ z₂) (by rw [← h₁₂, ← h₂, ← h, add_assoc]) +
n₂.negOnePow • (δ n₁ m₁ z₁).comp z₂ (by rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_assoc]) :=
by
subst h₁₂ h₁ h₂ h
ext p q hpq
dsimp
rw [z₁.comp_v _ (add_assoc n₁ n₂ 1).symm p _ q rfl (by cutsat),
Cochain.comp_v _ _ (show n₁ + 1 + n₂ = n₁ + n₂ + 1 by cutsat) p (p + n₁ + 1) q (by cutsat) (by cutsat),
δ_v (n₁ + n₂) _ rfl (z₁.comp z₂ rfl) p q hpq (p + n₁ + n₂) _ (by cutsat) rfl, z₁.comp_v z₂ rfl p _ _ rfl rfl,
z₁.comp_v z₂ rfl (p + 1) (p + n₁ + 1) q (by cutsat) (by cutsat),
δ_v n₂ (n₂ + 1) rfl z₂ (p + n₁) q (by cutsat) (p + n₁ + n₂) _ (by cutsat) rfl,
δ_v n₁ (n₁ + 1) rfl z₁ p (p + n₁ + 1) (by cutsat) (p + n₁) _ (by cutsat) rfl]
simp only [assoc, comp_add, add_comp, Int.negOnePow_succ, Int.negOnePow_add n₁ n₂, Units.neg_smul, comp_neg, neg_comp,
smul_neg, smul_smul, Linear.units_smul_comp, mul_comm n₁.negOnePow n₂.negOnePow, Linear.comp_units_smul, smul_add]
abel
