t-structures on triangulated categories

This files 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 type classes 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.{u_2, 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

theorem CategoryTheory.Triangulated.TStructure.exists_triangle {C : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : Monotone t.le

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

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

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

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

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

theorem CategoryTheory.Triangulated.TStructure.le_of_isLE {C : Type u_1} [Category.{u_2, 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.{u_2, 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

@[deprecated CategoryTheory.Triangulated.TStructure.le (since := "2025-02-25")]

def CategoryTheory.Triangulated.TStructure.LE {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (self : TStructure C) (n : ℤ) : ObjectProperty C

Alias of CategoryTheory.Triangulated.TStructure.le.

---

the predicate of objects that are ≤ n for n : ℤ.

Equations

• @CategoryTheory.Triangulated.TStructure.LE = @CategoryTheory.Triangulated.TStructure.le

@[deprecated CategoryTheory.Triangulated.TStructure.ge (since := "2025-02-25")]

def CategoryTheory.Triangulated.TStructure.GE {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (self : TStructure C) (n : ℤ) : ObjectProperty C

Alias of CategoryTheory.Triangulated.TStructure.ge.

---

the predicate of objects that are ≥ n for n : ℤ.

Equations

• @CategoryTheory.Triangulated.TStructure.GE = @CategoryTheory.Triangulated.TStructure.ge

@[deprecated CategoryTheory.Triangulated.TStructure.le_shift (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.LE_shift {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (self : TStructure C) (n a n' : ℤ) (h : a + n' = n) (X : C) (hX : self.le n X) : self.le n' ((shiftFunctor C a).obj X)

Alias of CategoryTheory.Triangulated.TStructure.le_shift.

@[deprecated CategoryTheory.Triangulated.TStructure.ge_shift (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.GE_shift {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (self : TStructure C) (n a n' : ℤ) (h : a + n' = n) (X : C) (hX : self.ge n X) : self.ge n' ((shiftFunctor C a).obj X)

Alias of CategoryTheory.Triangulated.TStructure.ge_shift.

@[deprecated CategoryTheory.Triangulated.TStructure.le_zero_le (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.LE_zero_le {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (self : TStructure C) : self.le 0 ≤ self.le 1

Alias of CategoryTheory.Triangulated.TStructure.le_zero_le.

@[deprecated CategoryTheory.Triangulated.TStructure.ge_one_le (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.GE_one_le {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (self : TStructure C) : self.ge 1 ≤ self.ge 0

Alias of CategoryTheory.Triangulated.TStructure.ge_one_le.

@[deprecated CategoryTheory.Triangulated.TStructure.shift_le (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.predicateShift_LE {C : Type u_1} [Category.{u_2, 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'

Alias of CategoryTheory.Triangulated.TStructure.shift_le.

@[deprecated CategoryTheory.Triangulated.TStructure.shift_ge (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.predicateShift_GE {C : Type u_1} [Category.{u_2, 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'

Alias of CategoryTheory.Triangulated.TStructure.shift_ge.

@[deprecated CategoryTheory.Triangulated.TStructure.le_monotone (since := "2025-02-25")]

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

Alias of CategoryTheory.Triangulated.TStructure.le_monotone.

@[deprecated CategoryTheory.Triangulated.TStructure.ge_antitone (since := "2025-02-25")]

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

Alias of CategoryTheory.Triangulated.TStructure.ge_antitone.

@[deprecated CategoryTheory.Triangulated.TStructure.le_of_isLE (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.mem_of_isLE {C : Type u_1} [Category.{u_2, 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

Alias of CategoryTheory.Triangulated.TStructure.le_of_isLE.

@[deprecated CategoryTheory.Triangulated.TStructure.ge_of_isGE (since := "2025-02-25")]

theorem CategoryTheory.Triangulated.TStructure.mem_of_isGE {C : Type u_1} [Category.{u_2, 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

Alias of CategoryTheory.Triangulated.TStructure.ge_of_isGE.