English
The localized category W.Localization is equipped with a triangulated structure: distinguished triangles are those in essImageDistTriang, there is a compatibility isomorphism, and the rotation, morphism completion, and other triangulated operations pass through the localization functor.
Русский
Локализованная категория W.Localization имеет триангулированную структуру: выделенные треугольники — это элементы essImageDistTriang, существуют совместимые изоморфизмы, вращение и другие операции проходят через функтор локализации.
LaTeX
$$$\text{Pretriangulated } W.Localization \ = \ \text{structure arising from } L: C\to D;\;\text{distinguished} = L.essImageDistTriang;\;\text{contractible} = \text{contractible}_{L}\text{distinguished}$$$
Lean4
/-- The pretriangulated structure on the localized category. -/
def pretriangulated : Pretriangulated D
where
distinguishedTriangles := L.essImageDistTriang
isomorphic_distinguished _ hT₁ _ e := L.essImageDistTriang_mem_of_iso e hT₁
contractible_distinguished :=
have := essSurj L W;
L.contractible_mem_essImageDistTriang
distinguished_cocone_triangle f := distinguished_cocone_triangle L W f
rotate_distinguished_triangle := L.rotate_essImageDistTriang
complete_distinguished_triangle_morphism := complete_distinguished_triangle_morphism L W
