mono_homologyMap_mor₁_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mono_homologyMap_mor₁_iff : Mono ((homologyFunctor C n₁).map T.mor₁) ↔ δ T n₀ n₁ h = 0 :=
  (homologyFunctor C 0).homologySequence_mono_shift_map_mor₁_iff _ hT _ _ h

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