binaryBiproductTriangle_distinguished

English

A triangle built from a binary biproduct is distinguished.

Русский

Треугольник, построенный из бинарного би-произведения, является распознаваемым.

LaTeX

$$$\\mathrm{binaryProductTriangle} X_1 X_2 \\in \\mathrm{distTriang} \\ C$$$

Lean4

theorem binaryBiproductTriangle_distinguished (X₁ X₂ : C) : binaryBiproductTriangle X₁ X₂ ∈ distTriang C :=
  by
  obtain ⟨Y, g, h, mem⟩ := distinguished_cocone_triangle₂ (0 : X₂ ⟶ X₁⟦(1 : ℤ)⟧)
  obtain ⟨e, ⟨he₁, he₂⟩⟩ := exists_iso_binaryBiproduct_of_distTriang _ mem rfl
  dsimp at he₁ he₂
  refine isomorphic_distinguished _ mem _ (Iso.symm ?_)
  refine Triangle.isoMk _ _ (Iso.refl _) e (Iso.refl _) (by cat_disch) (by cat_disch) (by simp)

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