mapShortComplex₃_exact — Mathlib

English

The short complex H_i(G, X2) → H_i(G, X3) → H_j(G, X1) is exact for all i when X is a short exact sequence 0 → X1 → X2 → X3 → 0.

Русский

Короткий комплекс H_i(G, X2) → H_i(G, X3) → H_j(G, X1) точен для всех i, если X является коротко точной последовательностью 0 → X1 → X2 → X3 → 0.

LaTeX

$$$mapShortComplex₃_exact (hX) (hij) : (mapShortComplex₃ hX hij).Exact$$$

Lean4

/-- Exactness of `Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁)`. -/
theorem mapShortComplex₃_exact {i j : ℕ} (hij : j + 1 = i) : (mapShortComplex₃ hX hij).Exact :=
  (map_chainsFunctor_shortExact hX).homology_exact₃ i j hij

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