mapShortComplex₁_exact — Mathlib

English

For i,j with i+1 = j, the mapShortComplex₁ applied to hX gives an exact sequence.

Русский

При i+1 = j отображение mapShortComplex₁ применённое к hX образует точную последовательность.

LaTeX

$$(mapShortComplex₁ hX hij).Exact$$

Lean4

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

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