contractible_distinguished₂ — Mathlib

English

For any distinguished triangle, a morphism from X to T.obj₂ that composes to zero with mor₂ factors through T.obj₁ via mor₁.

Русский

Для любого выделенного треугольника морфизм X → T.obj₂, композиция с mor₂ равна нулю, факторизуется через T.obj₁ через mor₁.

LaTeX

$$yoneda_exact₂$$

Lean4

/-- Obvious triangles `X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧` are distinguished -/
theorem contractible_distinguished₂ (X : C) : Triangle.mk (0 : X ⟶ 0) 0 (𝟙 (X⟦1⟧)) ∈ distTriang C :=
  by
  refine isomorphic_distinguished _ (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_
  exact
    Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
      (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])

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