mor₁_eq_zero_iff_epi₃ — Mathlib

English

In a distinguished triangle, mor1 is zero if and only if mor3 is epi; the two conditions are equivalent given the triangulated structure.

Русский

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

LaTeX

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

Lean4

theorem mor₁_eq_zero_iff_epi₃ : T.mor₁ = 0 ↔ Epi T.mor₃ :=
  by
  have h := mor₃_eq_zero_iff_epi₂ _ (rot_of_distTriang _ hT)
  dsimp at h
  rw [← h, neg_eq_zero]
  constructor
  · intro h
    simp only [h, Functor.map_zero]
  · intro h
    rw [← (CategoryTheory.shiftFunctor C (1 : ℤ)).map_eq_zero_iff, h]

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