English
The v-component of the composite z1.comp z2 is given by the product of the v-components with the degree shifts: (z1.comp z2 h).v(p1,p3) = z1.v(p1,p2) h1 ∘ z2.v(p2,p3) h2 for p1+n1 = p2 and p2+n2 = p3.
Русский
v-компонента композиции задаётся произведением компонент v с учётом сдвигов степеней: (z1.comp z2 h).v(p1,p3) = z1.v(p1,p2) h1 ∘ z2.v(p2,p3) h2 при p1+n1 = p2 и p2+n2 = p3.
LaTeX
$$$$ (z_1.comp z_2 h).v(p_1,p_3) = z_1.v(p_1,p_2)\,h_1 \;\circ\; z_2.v(p_2,p_3)\,h_2, $$
where $h$ encodes $n_1+n_2=n_{12}$, $h_1:p_1+n_1=p_2$, $h_2:p_2+n_2=p_3$.$$
Lean4
theorem comp_v {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (p₁ p₂ p₃ : ℤ)
(h₁ : p₁ + n₁ = p₂) (h₂ : p₂ + n₂ = p₃) :
(z₁.comp z₂ h).v p₁ p₃ (by rw [← h₂, ← h₁, ← h, add_assoc]) = z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂ := by subst h₁; rfl
