epi_homologyMap_mor₂_iff — Mathlib

English

Let T be as above with n0, n1 and h. The morphism (H_{n0}(T.mor2)) is epi if and only if δ_T n0 n1 h = 0.

Русский

Пусть T — как выше, с n0, n1 и h. Отображение (H_{n0}(T.mor2)) является эпиморфизмом тогда и только тогда, когда δ_T n0 n1 h = 0.

LaTeX

$$$$ \operatorname{Epi}\big((H_{n_0} (T.mor_2))\big) \iff \delta_T(n_0,n_1,h) = 0. $$$$

Lean4

theorem epi_homologyMap_mor₂_iff : Epi ((homologyFunctor C n₀).map T.mor₂) ↔ δ T n₀ n₁ h = 0 :=
  (homologyFunctor C 0).homologySequence_epi_shift_map_mor₂_iff _ hT _ _ h

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