English
In degree 0→1, the v-component of the differential applied to a zero-degree cochain z is given by the difference between the right and left actions of the differentials on the components, i.e., (δ 0 1 z).v_pq = z.v_pp (applied shift) ∘ G.d_pq − F.d_pq ∘ z.v_qq (shift).
Русский
В компоненте v нуля в единицу, дифференциал δ_{0,1} применённого коцепа z имеет вид: (δ 0 1 z).v_{p,q} = z.v_{p,p} (сдвиг) ∘ G.d_{p,q} − F.d_{p,q} ∘ z.v_{q,q} (сдвиг).
LaTeX
$$$(\delta\;0\;1\ z).v\;p\;q\;hpq = z.v\;p\;p\; (add_zero p) \;\gg\; G.d\;p\;q \\ &\qquad - F.d\;p\;q \gg z.v\;q\;q\; (add_zero q)$$$
Lean4
@[simp]
theorem δ_zero_cochain_v (z : Cochain F G 0) (p q : ℤ) (hpq : p + 1 = q) :
(δ 0 1 z).v p q hpq = z.v p p (add_zero p) ≫ G.d p q - F.d p q ≫ z.v q q (add_zero q) := by
simp only [δ_v 0 1 (zero_add 1) z p q hpq p q (by cutsat) hpq, Int.negOnePow_one, Units.neg_smul, one_smul,
sub_eq_add_neg]
