contractible_mem_essImageDistTriang

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)

Похожие утверждения