coyoneda_exact₁ — Mathlib

English

In a triangulated category with a distinguished triangle T, for any morphism f: X → T1(1) whose shifted composition with mor1(1) is zero, f factors through mor3; i.e., there exists g: X → T3 with f = g ∘ mor3.

Русский

В троянгированной категории с отличимым треугольником T, для любого гомоморфизма f: X → T1(1), для которого композиция f с mor1(1) равна нулю, существует г: X → T3 такой, что f = g ∘ mor3.

LaTeX

$$$\\forall X$, $f: X \\to T_{1}(1)$, $(f \\circ T_{m,1}(1)') = 0 \\ \Rightarrow\\ \\exists g: X \\to T_{3},\\ f = g \\circ T_{m,3}$$$

Lean4

theorem coyoneda_exact₁ {X : C} (f : X ⟶ T.obj₁⟦(1 : ℤ)⟧) (hf : f ≫ T.mor₁⟦1⟧' = 0) :
    ∃ (g : X ⟶ T.obj₃), f = g ≫ T.mor₃ :=
  coyoneda_exact₂ _ (rot_of_distTriang _ (rot_of_distTriang _ hT)) f (by cat_disch)

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