English
If a category has zero object and shift, then it has finite biproducts.
Русский
Если у категории есть нулевой объект и сдвиг, то она имеет конечные би-произведения.
LaTeX
$$$\\mathrm{HasFiniteBiproducts} \\, C$$$
Lean4
/-- A choice of isomorphism `T₁ ≅ T₂` between two distinguished triangles
when we are given two isomorphisms `e₁ : T₁.obj₁ ≅ T₂.obj₁` and `e₂ : T₁.obj₂ ≅ T₂.obj₂`. -/
@[simps! hom_hom₁ hom_hom₂ inv_hom₁ inv_hom₂]
def isoTriangleOfIso₁₂ (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distTriang C) (hT₂ : T₂ ∈ distTriang C) (e₁ : T₁.obj₁ ≅ T₂.obj₁)
(e₂ : T₁.obj₂ ≅ T₂.obj₂) (comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁) : T₁ ≅ T₂ :=
by
have h := exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk e₁ e₂ comm.symm)
exact
Triangle.isoMk _ _ e₁ e₂ (Triangle.π₃.mapIso h.choose) comm
(by
have eq := h.choose_spec.2
dsimp at eq ⊢
conv_rhs => rw [← eq, ← TriangleMorphism.comm₂])
(by
have eq := h.choose_spec.1
dsimp at eq ⊢
conv_lhs => rw [← eq, TriangleMorphism.comm₃])
