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

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

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

• LE : ℤ → C → Prop

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

• GE : ℤ → C → Prop

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

• LE_closedUnderIsomorphisms : ∀ (n : ℤ), CategoryTheory.ClosedUnderIsomorphisms (self.LE n)
• GE_closedUnderIsomorphisms : ∀ (n : ℤ), CategoryTheory.ClosedUnderIsomorphisms (self.GE n)
• LE_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), self.LE n X → self.LE n' ((CategoryTheory.shiftFunctor C a).obj X)
• GE_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), self.GE n X → self.GE n' ((CategoryTheory.shiftFunctor C a).obj X)
• zero' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), self.LE 0 X → 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 ⟶ (CategoryTheory.shiftFunctor C 1).obj X), CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Triangulated.TStructure.exists_triangle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.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 ⟶ (CategoryTheory.shiftFunctor C 1).obj X), CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

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

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

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

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

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

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