English
For a functor L that is a localization and preserves left calculus of fractions, a triangle T belongs to distTriang(D) iff T belongs to L.essImageDistTriang.
Русский
Для функторa L, являющегося локализацией и сохраняющего левую Латля-фракцию, треугольник T принадлежит distTriang(D) тогда и только тогда, когда T принадлежит L.essImageDistTriang.
LaTeX
$$$T\in distTriang(D) \iff T\in L.essImageDistTriang$$$
Lean4
theorem distTriang_iff (T : Triangle D) : (T ∈ distTriang D) ↔ T ∈ L.essImageDistTriang :=
by
constructor
· intro hT
let f := L.mapArrow.objPreimage T.mor₁
obtain ⟨Z, g : f.right ⟶ Z, h : Z ⟶ f.left⟦(1 : ℤ)⟧, mem⟩ := Pretriangulated.distinguished_cocone_triangle f.hom
exact
⟨_,
(exists_iso_of_arrow_iso T _ hT (L.map_distinguished _ mem) (L.mapArrow.objObjPreimageIso T.mor₁).symm).choose,
mem⟩
· rintro ⟨T₀, e, hT₀⟩
exact isomorphic_distinguished _ (L.map_distinguished _ hT₀) _ e
