mor₂_eq_zero_iff_epi₁ — Mathlib

English

Let T be a distinguished triangle. Then mor3 is zero if and only if mor2 is epi; equivalently, the right-hand morphism mor3 being zero exactly captures when mor2 is epic in a distinguished triangle.

Русский

Пусть T — отличный треугольник. Тогда mor3 = 0 тогда и только тогда, когда mor2 является эпиморфизмом; эквивалентно, нулевой mor3 точно описывает эпивность mor2 в отличимом треугольнике.

LaTeX

$$$T \\text{ distinguished} \\Rightarrow (T.mor_3 = 0) \\iff Epi(T.mor_2)$$$

Lean4

theorem mor₂_eq_zero_iff_epi₁ : T.mor₂ = 0 ↔ Epi T.mor₁ :=
  by
  have h := mor₃_eq_zero_iff_epi₂ _ (inv_rot_of_distTriang _ hT)
  dsimp at h
  rw [← h, IsIso.comp_right_eq_zero]

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