isTriangulated_functor — Mathlib

English

If L is a localization functor satisfying the localization hypotheses and compatibility with triangulation, then the localized functor is triangulated.

Русский

Если L является локализационным функтором, удовлетворяющим гипотезам локализации и совместимости с триангуляцией, то локализованный функтор является триангулированным.

LaTeX

$$$\text{IsTriangulated }(W.Localization') = \text{isTriangulated}(W.Q',W)$$$

Lean4

instance isTriangulated_functor :
    letI : Pretriangulated D := pretriangulated L W;
    L.IsTriangulated :=
  letI : Pretriangulated D := pretriangulated L W
  ⟨fun T hT => ⟨T, Iso.refl _, hT⟩⟩

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