Triangulated subcategories

In this file, we introduce the notion of triangulated subcategory of a pretriangulated category C. If S : Subcategory W, we define the class of morphisms S.W : MorphismProperty C consisting of morphisms whose "cone" belongs to S (up to isomorphisms). We show that S.W has both calculus of left and right fractions.

TODO

• obtain (pre)triangulated instances on the localized category with respect to S.W
• define the type S.category as Fullsubcategory S.set and show that it is a pretriangulated category.

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₂

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₂

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] (S : CategoryTheory.Triangulated.Subcategory C) [CategoryTheory.ClosedUnderIsomorphisms S.P] : S.P 0

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) : CategoryTheory.Triangulated.Subcategory C

The closure under isomorphisms of a triangulated subcategory.

Equations

• S.isoClosure = { P := CategoryTheory.isoClosure S.P, zero' := ⋯, shift := ⋯, ext₂' := ⋯ }

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₂) : CategoryTheory.Triangulated.Subcategory C

An alternative constructor for "strictly full" triangulated subcategory.

Equations

• CategoryTheory.Triangulated.Subcategory.mk' P zero shift ext₂ = { P := P, zero' := ⋯, shift := shift, ext₂' := ⋯ }

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₂

def CategoryTheory.Triangulated.Subcategory.W {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.MorphismProperty C

Given S : Triangulated.Subcategory C, this is the class of morphisms on C which consists of morphisms whose cone satisfies S.P.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.Subcategory.W_iff {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) {X : C} {Y : C} (f : X ⟶ Y) : S.W f ↔ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), S.P Z

theorem CategoryTheory.Triangulated.Subcategory.W_iff' {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) {Y : C} {Z : C} (g : Y ⟶ Z) : S.W g ↔ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), S.P X

theorem CategoryTheory.Triangulated.Subcategory.W.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] (S : CategoryTheory.Triangulated.Subcategory C) {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : S.P T.obj₃) : S.W T.mor₁

theorem CategoryTheory.Triangulated.Subcategory.W.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] (S : CategoryTheory.Triangulated.Subcategory C) {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : S.P T.obj₁) : S.W T.mor₂

theorem CategoryTheory.Triangulated.Subcategory.isoClosure_W {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) : S.isoClosure.W = S.W

theorem CategoryTheory.Triangulated.Subcategory.respectsIso_W {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) : S.W.RespectsIso

instance CategoryTheory.Triangulated.Subcategory.instContainsIdentitiesW {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) : S.W.ContainsIdentities

Equations

• ⋯ = ⋯

theorem CategoryTheory.Triangulated.Subcategory.W_of_isIso {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) {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : S.W f

theorem CategoryTheory.Triangulated.Subcategory.smul_mem_W_iff {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) {X : C} {Y : C} (f : X ⟶ Y) (n : ℤˣ) : S.W (n • f) ↔ S.W f

theorem CategoryTheory.Triangulated.Subcategory.W.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] {S : CategoryTheory.Triangulated.Subcategory C} {X₁ : C} {X₂ : C} {f : X₁ ⟶ X₂} (hf : S.W f) (n : ℤ) : S.W ((CategoryTheory.shiftFunctor C n).map f)

theorem CategoryTheory.Triangulated.Subcategory.W.unshift {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} {X₁ : C} {X₂ : C} {f : X₁ ⟶ X₂} {n : ℤ} (hf : S.W ((CategoryTheory.shiftFunctor C n).map f)) : S.W f

instance CategoryTheory.Triangulated.Subcategory.instIsCompatibleWithShiftWInt {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} : S.W.IsCompatibleWithShift ℤ

Equations

• ⋯ = ⋯

instance CategoryTheory.Triangulated.Subcategory.instIsMultiplicativeWOfIsTriangulated {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.IsTriangulated C] : S.W.IsMultiplicative

Equations

• ⋯ = ⋯

theorem CategoryTheory.Triangulated.Subcategory.mem_W_iff_of_distinguished {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) : S.W T.mor₁ ↔ S.P T.obj₃

instance CategoryTheory.Triangulated.Subcategory.instHasLeftCalculusOfFractionsWOfIsTriangulated {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.IsTriangulated C] : S.W.HasLeftCalculusOfFractions

Equations

• ⋯ = ⋯

instance CategoryTheory.Triangulated.Subcategory.instHasRightCalculusOfFractionsWOfIsTriangulated {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.IsTriangulated C] : S.W.HasRightCalculusOfFractions

Equations

• ⋯ = ⋯

instance CategoryTheory.Triangulated.Subcategory.instIsCompatibleWithTriangulationWOfIsTriangulated {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.IsTriangulated C] : S.W.IsCompatibleWithTriangulation

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) (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) [CategoryTheory.ClosedUnderIsomorphisms S.P] (h₂ : S.P T.obj₂) (h₃ : S.P T.obj₃) : S.P T.obj₁

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) (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) [CategoryTheory.ClosedUnderIsomorphisms S.P] (h₁ : S.P T.obj₁) (h₂ : S.P T.obj₂) : S.P T.obj₃

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) (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : S.P T.obj₂) (h₃ : S.P T.obj₃) : CategoryTheory.isoClosure S.P T.obj₁

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) (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : S.P T.obj₁) (h₂ : S.P T.obj₂) : CategoryTheory.isoClosure S.P T.obj₃