comp_assoc_of_second_is_zero_cochain

English

If z1 is a zero cochain of degree 0, then (z1.comp z2 h12).comp z3 h23 = z1.comp (z2.comp z3 h23) with h12, h23 appropriate; first cochain zero simplifies the associativity.

Русский

Если z1 — нулевой коцепоинт степени 0, то (z1.comp z2 h12).comp z3 h23 = z1.comp (z2.comp z3 h23).

LaTeX

$$$$ (z_1.comp z_2 h_{12}).comp z_3 h_{23} = z_1.comp (z_2.comp z_3 h_{23}) \,.$$$$

Lean4

@[simp]
theorem comp_assoc_of_second_is_zero_cochain {n₁ n₃ n₁₃ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K 0)
    (z₃ : Cochain K L n₃) (h₁₃ : n₁ + n₃ = n₁₃) :
    (z₁.comp z₂ (add_zero n₁)).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ (zero_add n₃)) h₁₃ :=
  comp_assoc _ _ _ _ _ (by cutsat)

Похожие утверждения