epi_homologyMap_mor₁_iff — Mathlib

English

Let T be a distinguished triangle in the derived category of C, and let n0 be an integer. Then the morphism (H_{n0} (T.mor1)) is epi if and only if (H_{n0} (T.mor2)) = 0.

Русский

Пусть T — отличимая треугольная диаграмма в производной категории C, и возьмем целое число n0. Тогда отображение (H_{n0}(T.mor1)) является эпиморфизмом тогда и только тогда, когда (H_{n0}(T.mor2)) = 0.

LaTeX

$$$$ \operatorname{Epi}\big((H_{n_0} (T.mor_1))\big) \iff (H_{n_0} (T.mor_2)) = 0. $$$$

Lean4

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

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