Documentation

Mathlib.CategoryTheory.Triangulated.TStructure.Basic

t-structures on triangulated categories #

This file introduces the notion of t-structure on (pre)triangulated categories.

The first example of t-structure shall be the canonical t-structure on the derived category of an abelian category (TODO).

Given a t-structure t : TStructure C, we define typeclasses t.IsLE X n and t.IsGE X n in order to say that an object X : C is ≤ n or ≥ n for t.

Implementation notes #

We introduce the type of t-structures rather than a type class saying that we have fixed a t-structure on a certain category. The reason is that certain triangulated categories have several t-structures which one may want to use depending on the context.

TODO #

define functors t.truncLE n : C ⥤ C, t.truncGE n : C ⥤ C and the associated distinguished triangles
promote these truncations to a (functorial) spectral object
define the heart of t and show it is an abelian category
define triangulated subcategories t.plus, t.minus, t.bounded and show that there are induced t-structures on these full subcategories

References #

[Beilinson, Bernstein, Deligne, Gabber, Faisceaux pervers][bbd-1982]

structure CategoryTheory.Triangulated.TStructure (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] :

Type u_1

TStructure C is the type of t-structures on the (pre)triangulated category C.

le (n : ℤ) : ObjectProperty C
the predicate of objects that are ≤ n for n : ℤ.
ge (n : ℤ) : ObjectProperty C
the predicate of objects that are ≥ n for n : ℤ.
le_isClosedUnderIsomorphisms (n : ℤ) : (self.le n).IsClosedUnderIsomorphisms
ge_isClosedUnderIsomorphisms (n : ℤ) : (self.ge n).IsClosedUnderIsomorphisms
le_shift (n a n' : ℤ) (h : a + n' = n) (X : C) (hX : self.le n X) : self.le n' ((shiftFunctor C a).obj X)
ge_shift (n a n' : ℤ) (h : a + n' = n) (X : C) (hX : self.ge n X) : self.ge n' ((shiftFunctor C a).obj X)
zero' ⦃X Y : C⦄ (f : X ⟶ Y) (hX : self.le 0 X) (hY : self.ge 1 Y) : f = 0
le_zero_le : self.le 0 ≤ self.le 1
ge_one_le : self.ge 1 ≤ self.ge 0
exists_triangle_zero_one (A : C) : ∃ (X : C) (Y : C) (_ : self.le 0 X) (_ : self.ge 1 Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

Instances For

theorem CategoryTheory.Triangulated.TStructure.exists_triangle {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (A : C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :

∃ (X : C) (Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Triangulated.TStructure.shift_le {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n n' : ℤ) (hn' : a + n = n') :

(t.le n).shift a = t.le n'

theorem CategoryTheory.Triangulated.TStructure.shift_ge {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a n n' : ℤ) (hn' : a + n = n') :

(t.ge n).shift a = t.ge n'

theorem CategoryTheory.Triangulated.TStructure.le_monotone {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

theorem CategoryTheory.Triangulated.TStructure.ge_antitone {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

class CategoryTheory.Triangulated.TStructure.IsLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) :

Given a t-structure t on a pretriangulated category C, the property t.IsLE X n holds if X : C is ≤ n for the t-structure.

le : t.le n X

Instances

class CategoryTheory.Triangulated.TStructure.IsGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) :

Given a t-structure t on a pretriangulated category C, the property t.IsGE X n holds if X : C is ≥ n for the t-structure.

ge : t.ge n X

Instances

theorem CategoryTheory.Triangulated.TStructure.le_of_isLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) [t.IsLE X n] :

t.le n X

theorem CategoryTheory.Triangulated.TStructure.ge_of_isGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) [t.IsGE X n] :

t.ge n X

theorem CategoryTheory.Triangulated.TStructure.isLE_of_iso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (e : X ≅ Y) (n : ℤ) [t.IsLE X n] :

t.IsLE Y n

theorem CategoryTheory.Triangulated.TStructure.isGE_of_iso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (e : X ≅ Y) (n : ℤ) [t.IsGE X n] :

t.IsGE Y n

theorem CategoryTheory.Triangulated.TStructure.isLE_of_le {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (p q : ℤ) (hpq : p ≤ q := by lia) [t.IsLE X p] :

t.IsLE X q

theorem CategoryTheory.Triangulated.TStructure.isGE_of_ge {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (p q : ℤ) (hpq : p ≤ q := by lia) [t.IsGE X q] :

t.IsGE X p

@[deprecated CategoryTheory.Triangulated.TStructure.isLE_of_le (since := "2026-01-30")]

theorem CategoryTheory.Triangulated.TStructure.isLE_of_LE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (p q : ℤ) (hpq : p ≤ q := by lia) [t.IsLE X p] :

t.IsLE X q

Alias of CategoryTheory.Triangulated.TStructure.isLE_of_le.

@[deprecated CategoryTheory.Triangulated.TStructure.isGE_of_ge (since := "2026-01-30")]

theorem CategoryTheory.Triangulated.TStructure.isGE_of_GE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (p q : ℤ) (hpq : p ≤ q := by lia) [t.IsGE X q] :

t.IsGE X p

Alias of CategoryTheory.Triangulated.TStructure.isGE_of_ge.

theorem CategoryTheory.Triangulated.TStructure.isLE_shift {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsLE X n] :

t.IsLE ((shiftFunctor C a).obj X) n'

theorem CategoryTheory.Triangulated.TStructure.isGE_shift {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsGE X n] :

t.IsGE ((shiftFunctor C a).obj X) n'

theorem CategoryTheory.Triangulated.TStructure.isLE_of_shift {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsLE ((shiftFunctor C a).obj X) n'] :

t.IsLE X n

theorem CategoryTheory.Triangulated.TStructure.isGE_of_shift {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsGE ((shiftFunctor C a).obj X) n'] :

t.IsGE X n

theorem CategoryTheory.Triangulated.TStructure.isLE_shift_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) :

t.IsLE ((shiftFunctor C a).obj X) n' ↔ t.IsLE X n

theorem CategoryTheory.Triangulated.TStructure.isGE_shift_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) :

t.IsGE ((shiftFunctor C a).obj X) n' ↔ t.IsGE X n

theorem CategoryTheory.Triangulated.TStructure.zero {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ < n₁ := by lia) [t.IsLE X n₀] [t.IsGE Y n₁] :

f = 0

theorem CategoryTheory.Triangulated.TStructure.zero_of_isLE_of_isGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ < n₁) :

t.IsLE X n₀ → t.IsGE Y n₁ → f = 0

theorem CategoryTheory.Triangulated.TStructure.isZero {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n₀ n₁ : ℤ) (h : n₀ < n₁ := by lia) [t.IsLE X n₀] [t.IsGE X n₁] :

Limits.IsZero X

def CategoryTheory.Triangulated.TStructure.minus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

ObjectProperty C

The full subcategory consisting of t-bounded above objects.

Equations

Instances For

def CategoryTheory.Triangulated.TStructure.plus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

ObjectProperty C

The full subcategory consisting of t-bounded below objects.

Equations

Instances For

def CategoryTheory.Triangulated.TStructure.bounded {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

ObjectProperty C

The full subcategory consisting of t-bounded objects.

Equations

Instances For

instance CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsMinus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

t.minus.IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftMinusInt {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

t.minus.IsStableUnderShift ℤ

instance CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsPlus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

t.plus.IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftPlusInt {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

t.plus.IsStableUnderShift ℤ

instance CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsBounded {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

t.bounded.IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftBoundedInt {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :

t.bounded.IsStableUnderShift ℤ