English
For every object X in D, the contractible triangle on X lies in essImageDistTriang of the localization L.
Русский
Для каждого объекта X в D треугольник,-contractibleTriangle X, принадлежит essImageDistTriang локализации L.
LaTeX
$$$\text{contractibleTriangle}(X) \in L.essImageDistTriang$ for all $X\in D$$$
Lean4
theorem contractible_mem_essImageDistTriang [EssSurj L] [HasZeroObject D] [HasZeroMorphisms D]
[L.PreservesZeroMorphisms] (X : D) : contractibleTriangle X ∈ L.essImageDistTriang :=
by
refine ⟨contractibleTriangle (L.objPreimage X), ?_, contractible_distinguished _⟩
exact
((contractibleTriangleFunctor D).mapIso (L.objObjPreimageIso X)).symm ≪≫
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) L.mapZeroObject.symm (by simp) (by simp) (by simp)