homology_exact₃ — Mathlib

English

For indices i, j with the relation c.Rel i j, the sequence H_i(S.X2) → H_i(S.X3) → H_i(S.X1) is exact with the δ morphism δ i j hij connecting H_i(S.X3) to H_j(S.X1).

Русский

Для индексов i, j с отношением c.Rel i j последовательность H_i(S.X2) → H_i(S.X3) → H_i(S.X1) точна, причём отображение δ i j hij соединяет H_i(S.X3) с H_j(S.X1).

LaTeX

$$$\\operatorname{Im}\\big(\\operatorname{HomologyMap}\\, S.g\\, i\\big) = \\ker\\big( hS.\\delta\\, i\\ j\\ hij \\big)$$

Lean4

/-- Exactness of `S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j`. -/
theorem homology_exact₃ : (ShortComplex.mk _ _ (comp_δ hS i j hij)).Exact :=
  (snakeInput hS i j hij).L₁'_exact

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