distinguished_cocone_triangle — Mathlib

English

In the HomotopyCategory, mappingCone.triangleh f is a distinguished triangle.

Русский

В гомотопийной категории треугольник mappingCone.triangleh f является выделенным.

LaTeX

$$$\\mathrm{mappingConetrianglehDistinguished}(f)$$$

Lean4

theorem distinguished_cocone_triangle {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y) :
    ∃ (Z : HomotopyCategory C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h : Z ⟶ X⟦1⟧),
      Triangle.mk f g h ∈ distinguishedTriangles C :=
  by
  obtain ⟨f, rfl⟩ := (quotient _ _).map_surjective f
  exact ⟨_, _, _, ⟨_, _, f, ⟨Iso.refl _⟩⟩⟩

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