Triangulated subcategories #
In this file, we introduce the notion of triangulated subcategory of a pretriangulated category.
TODO #
- define the class of morphisms whose "cone" belong to a subcategory
- obtain (pre)triangulated instances on the corresponding localized categories
Implementation notes #
In the definition of Triangulated.Subcategory, we do not assume that the predicate
on objects is closed under isomorphisms (i.e. that the subcategory is "strictly full").
Part of the theory would be more convenient under this stronger assumption
(e.g. Subcategory C would be a lattice), but some applications require this:
for example, the subcategory of bounded below complexes in the homotopy category
of an additive category is not closed under isomorphisms.
References #
- [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]
structure
CategoryTheory.Triangulated.Subcategory
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
:
Type u_1
A triangulated subcategory of a pretriangulated category C consists of
a predicate P : C → Prop which contains a zero object, is stable by shifts, and such that
if X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ is a distinguished triangle such that if X₁ and X₃ satisfy
P then X₂ is isomorphic to an object satisfying P.
- P : C → Prop
the underlying predicate on objects of a triangulated subcategory
- zero' : ∃ (Z : C) (_ : CategoryTheory.Limits.IsZero Z), self.P Z
- shift : ∀ (X : C) (n : ℤ), self.P X → self.P ((CategoryTheory.shiftFunctor C n).obj X)
- ext₂' : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, self.P T.obj₁ → self.P T.obj₃ → CategoryTheory.isoClosure self.P T.obj₂
Instances For
theorem
CategoryTheory.Triangulated.Subcategory.zero'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(self : CategoryTheory.Triangulated.Subcategory C)
:
∃ (Z : C) (_ : CategoryTheory.Limits.IsZero Z), self.P Z
theorem
CategoryTheory.Triangulated.Subcategory.shift
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(self : CategoryTheory.Triangulated.Subcategory C)
(X : C)
(n : ℤ)
:
self.P X → self.P ((CategoryTheory.shiftFunctor C n).obj X)
theorem
CategoryTheory.Triangulated.Subcategory.ext₂'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(self : CategoryTheory.Triangulated.Subcategory C)
(T : CategoryTheory.Pretriangulated.Triangle C)
:
T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
self.P T.obj₁ → self.P T.obj₃ → CategoryTheory.isoClosure self.P T.obj₂
def
CategoryTheory.Triangulated.Subcategory.isoClosure
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(S : CategoryTheory.Triangulated.Subcategory C)
:
The closure of a triangulated subcategory
Equations
- S.isoClosure = { P := CategoryTheory.isoClosure S.P, zero' := ⋯, shift := ⋯, ext₂' := ⋯ }
Instances For
instance
CategoryTheory.Triangulated.Subcategory.instClosedUnderIsomorphismsPIsoClosure
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(S : CategoryTheory.Triangulated.Subcategory C)
:
CategoryTheory.ClosedUnderIsomorphisms S.isoClosure.P
Equations
- ⋯ = ⋯
def
CategoryTheory.Triangulated.Subcategory.mk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(P : C → Prop)
(zero : P 0)
(shift : ∀ (X : C) (n : ℤ), P X → P ((CategoryTheory.shiftFunctor C n).obj X))
(ext₂ : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂)
:
An alternative constructor for "strictly full" triangulated subcategory.
Equations
- CategoryTheory.Triangulated.Subcategory.mk' P zero shift ext₂ = { P := P, zero' := ⋯, shift := shift, ext₂' := ⋯ }
Instances For
instance
CategoryTheory.Triangulated.Subcategory.instClosedUnderIsomorphismsPMk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(P : C → Prop)
(zero : P 0)
(shift : ∀ (X : C) (n : ℤ), P X → P ((CategoryTheory.shiftFunctor C n).obj X))
(ext₂ : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂)
:
CategoryTheory.ClosedUnderIsomorphisms (CategoryTheory.Triangulated.Subcategory.mk' P zero shift ext₂).P
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Triangulated.Subcategory.ext₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(S : CategoryTheory.Triangulated.Subcategory C)
[CategoryTheory.ClosedUnderIsomorphisms S.P]
(T : CategoryTheory.Pretriangulated.Triangle C)
(hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(h₁ : S.P T.obj₁)
(h₃ : S.P T.obj₃)
:
S.P T.obj₂