English
If Arrow.mk T1.mor1 ≅ Arrow.mk T2.mor1 isomorphism exists, there is an isomorphism T1 ≅ T2 extending it.
Русский
Если существует изоморфизм Arrow.mk T1.mor1 ≅ Arrow.mk T2.mor1, то существует изоморфизм T1 ≅ T2, совместимый с ним.
LaTeX
$$$\\exists e' : T_1 \\cong T_2, \\; e'.hom_1 = \\text{left}, e'.hom_2 = \\text{right}$$$
Lean4
theorem exists_iso_of_arrow_iso (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distTriang C) (hT₂ : T₂ ∈ distTriang C)
(e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁) :
∃ (e' : T₁ ≅ T₂), e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right :=
by
let φ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ e.hom.left e.hom.right e.hom.w.symm
have : IsIso φ.hom₁ := by dsimp [φ]; infer_instance
have : IsIso φ.hom₂ := by dsimp [φ]; infer_instance
have : IsIso φ.hom₃ := isIso₃_of_isIso₁₂ φ hT₁ hT₂ inferInstance inferInstance
have : IsIso φ := by
apply Triangle.isIso_of_isIsos
all_goals infer_instance
exact ⟨asIso φ, by simp [φ], by simp [φ]⟩
