instIsTriangulatedLocalization — Mathlib

English

The localized category W.Localization carries a pretriangulated structure, inherited from the source category via the localization functor.

Русский

Локализованная категория W.Localization имеет предтриангулированную структуру, восходящую к исходной через локализационный функтор.

LaTeX

$$$\text{Pretriangulated } W.Localization$$$

Lean4

instance [IsTriangulated C] : IsTriangulated W.Localization :=
  isTriangulated W.Q W

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