mapShortComplex₂_exact — Mathlib

English

The short complex H_i(G, X1) → H_i(G, X2) → H_i(G, X3) is exact for every i, given a short exact sequence 0 → X1 → X2 → X3 → 0.

Русский

Короткий комплекс H_i(G, X1) → H_i(G, X2) → H_i(G, X3) точен для каждого i, при условии, что 0 → X1 → X2 → X3 → 0 точна.

LaTeX

$$$mapShortComplex₂_exact (i) : (mapShortComplex₂ X i).Exact$$$

Lean4

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

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