Documentation

Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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) [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

Instances For

theorem CategoryTheory.Triangulated.TStructure.LE_closedUnderIsomorphisms {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] (self : CategoryTheory.Triangulated.TStructure C) (n : ℤ) :

CategoryTheory.ClosedUnderIsomorphisms (self.LE n)

theorem CategoryTheory.Triangulated.TStructure.GE_closedUnderIsomorphisms {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] (self : CategoryTheory.Triangulated.TStructure C) (n : ℤ) :

CategoryTheory.ClosedUnderIsomorphisms (self.GE n)

theorem CategoryTheory.Triangulated.TStructure.LE_shift {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] (self : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (a : ℤ) (n' : ℤ) (h : a + n' = n) (X : C) (hX : self.LE n X) :

self.LE n' ((CategoryTheory.shiftFunctor C a).obj X)

theorem CategoryTheory.Triangulated.TStructure.GE_shift {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] (self : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (a : ℤ) (n' : ℤ) (h : a + n' = n) (X : C) (hX : self.GE n X) :

self.GE n' ((CategoryTheory.shiftFunctor C a).obj X)

theorem CategoryTheory.Triangulated.TStructure.zero' {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] (self : CategoryTheory.Triangulated.TStructure C) ⦃X : C⦄ ⦃Y : C⦄ (f : X ⟶ Y) (hX : self.LE 0 X) (hY : self.GE 1 Y) :

f = 0

theorem CategoryTheory.Triangulated.TStructure.LE_zero_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] (self : CategoryTheory.Triangulated.TStructure C) :

self.LE 0 ≤ self.LE 1

theorem CategoryTheory.Triangulated.TStructure.GE_one_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] (self : CategoryTheory.Triangulated.TStructure C) :

self.GE 1 ≤ self.GE 0

theorem CategoryTheory.Triangulated.TStructure.exists_triangle_zero_one {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] (self : CategoryTheory.Triangulated.TStructure C) (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) :

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) :

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 : ℤ) :

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

theorem CategoryTheory.Triangulated.TStructure.IsLE.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} {X : C} {n : ℤ} [self : t.IsLE X n] :

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 : ℤ) :

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.IsGE.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} {X : C} {n : ℤ} [self : t.IsGE X n] :

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