English
The descended cochain differential splits into left and right contributions according to the cone data.
Русский
Дифференциал descended-cochain делится на левый и правый вклад согласно данным конуса.
LaTeX
$$$ δ_{descCochain} = (fst\\,φ).1 \\circ (δ_{m n} α + n'.negOnePow · (Cochain.ofHom φ) \\circ β) + (snd φ) \\circ δ_{n n'} β $$$
Lean4
theorem δ_descCochain (n' : ℤ) (hn' : n + 1 = n') :
δ n n' (descCochain φ α β h) =
(fst φ).1.comp (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β (zero_add n)) (by cutsat) +
(snd φ).comp (δ n n' β) (zero_add n') :=
by
dsimp only [descCochain]
simp only [δ_add, Cochain.comp_add, δ_comp (fst φ).1 α _ 2 n n' hn' (by cutsat) (by cutsat), Cocycle.δ_eq_zero,
Cochain.zero_comp, smul_zero, add_zero, δ_comp (snd φ) β (zero_add n) 1 n' n' hn' (zero_add 1) hn', δ_snd,
Cochain.neg_comp, smul_neg, Cochain.comp_assoc_of_second_is_zero_cochain, Cochain.comp_units_smul, ← hn',
Int.negOnePow_succ, Units.neg_smul, Cochain.comp_neg]
abel
