English
Dual Yoneda-type exactness: from a morphism to the second object of the triangle that becomes zero after composing with mor₂, one obtains a factorization through mor₁.
Русский
Тождество точности типаCoyoneda: из морфизма в второй объект треугольника, который становится нулём после композиции с mor₂, следует факторизация через mor₁.
LaTeX
$$coyoneda_exact₂$$
Lean4
/-- Any morphism `Z ⟶ X⟦1⟧` is part of a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` -/
theorem distinguished_cocone_triangle₂ {Z X : C} (h : Z ⟶ X⟦(1 : ℤ)⟧) :
∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z), Triangle.mk f g h ∈ distTriang C :=
by
obtain ⟨Y', f', g', mem⟩ := distinguished_cocone_triangle h
let T' := (Triangle.mk h f' g').invRotate.invRotate
refine
⟨T'.obj₂, ((shiftEquiv C (1 : ℤ)).unitIso.app X).hom ≫ T'.mor₁, T'.mor₂,
isomorphic_distinguished _ (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ mem)) _ ?_⟩
exact
Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _) (by cat_disch) (by cat_disch)
(by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])
