d₃₂_comp_d₂₁ — Mathlib

English

In group homology, the successive boundary maps d32 and d21 compose to zero.

Русский

В последовательной цепи гомологии границы удовлетворяют d32 ∘ d21 = 0.

LaTeX

$$$d_{32} \\circ d_{21} = 0$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem d₃₂_comp_d₂₁ : d₃₂ A ≫ d₂₁ A = 0 := by
  simp [← cancel_mono (chainsIso₁ A).inv, ← eq_d₂₁_comp_inv, ← eq_d₃₂_comp_inv_assoc]

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