mapShortComplex₁_exact — Mathlib

English

The short complex H_i(G, X3) → H_j(G, X1) → H_j(G, X2) is exact, i.e., the image of the first map equals the kernel of the second.

Русский

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

LaTeX

$$$(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

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