coyoneda_exact₃ — Mathlib

English

In a distinguished triangle T, for any f: X → T3 with f composed with mor3 equal to zero, there exists g: X → T2 such that f = g ∘ mor2; i.e., mor2 is a universal source for zero composites with mor3.

Русский

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

LaTeX

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

Lean4

theorem coyoneda_exact₃ {X : C} (f : X ⟶ T.obj₃) (hf : f ≫ T.mor₃ = 0) : ∃ (g : X ⟶ T.obj₂), f = g ≫ T.mor₂ :=
  coyoneda_exact₂ _ (rot_of_distTriang _ hT) f hf

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