mapShortComplex₃_exact — Mathlib

English

The third short complex H^i(G,X2) → H^i(G,X3) → H^j(G,X1) is exact, coming from the underlying short exact sequence.

Русский

Третья краткая когомологическая последовательность точна, происходит из исходной точной последовательности.

LaTeX

$${i j: natural numbers} → (mapShortComplex3 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

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