contractible_distinguished — Mathlib

English

For any morphism f in the homotopy category, there exists a distinguished cocone triangle with vertex at the domain/codomain, i.e., a mapping-cone-style distinguished triangle associated to f.

Русский

Для любого морфизма f в гомотопийной категории существует выделенный кокон-треугольник, т.е. треугольник-конус отображения, соответствующий f.

LaTeX

$$$\\exists Z\\, g\\, h:\\; \\text{Triangle.mk}(f,g,h) \\in \\text{distinguishedTriangles}$$$

Lean4

theorem contractible_distinguished (X : HomotopyCategory C (ComplexShape.up ℤ)) :
    Pretriangulated.contractibleTriangle X ∈ distinguishedTriangles C :=
  by
  obtain ⟨X⟩ := X
  refine ⟨_, _, 𝟙 X, ⟨?_⟩⟩
  have h := (isZero_quotient_obj_iff _).2 ⟨CochainComplex.mappingCone.homotopyToZeroOfId X⟩
  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) h.isoZero.symm (by simp) (h.eq_of_tgt _ _) (by dsimp; ext)

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