English
If P is triangulated, then the iso-closure construction yields P.IsTriangulatedClosed₂, i.e., the first two vertices determine the closure of the third under distinguished triangles.
Русский
Если P является треангулированным, то конструирование isoClosure даёт P.IsTriangulatedClosed₂, то есть первые две вершины определяют замыкание третьего в рамках выделенных треугольников.
LaTeX
$$$P.IsTriangulatedClosed₂ \\text{ holds because } P.ext_of_isTriangulatedClosed₂'$, hence isoClosure preserves triangulated closure.$$
Lean4
instance [P.IsTriangulatedClosed₂] : P.isoClosure.IsTriangulatedClosed₂ where
ext₂' := by
rintro T hT ⟨X₁, h₁, ⟨e₁⟩⟩ ⟨X₃, h₃, ⟨e₃⟩⟩
exact
ObjectProperty.le_isoClosure _ _
(P.ext_of_isTriangulatedClosed₂'
(Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ e₁.hom⟦1⟧'))
(isomorphic_distinguished _ hT _
(Triangle.isoMk _ _ e₁.symm (Iso.refl _) e₃.symm (by simp) (by simp)
(by
dsimp
simp only [assoc, ← Functor.map_comp, e₁.hom_inv_id, Functor.map_id, comp_id])))
h₁ h₃)
