Triangulated subcategories

In this file, given a pretriangulated category C and P : ObjectProperty C, we introduce a typeclass P.IsTriangulated to express that P is a triangulated subcategory of C. When P is a triangulated subcategory, we introduce a class of morphisms P.trW : MorphismProperty C consisting of the morphisms whose "cone" belongs to P (up to isomorphisms), and we show that it has both calculus of left and right fractions.

TODO

• show that the fullsubcategory attached to P (such that P.IsTriangulated) is a pretriangulated category.

Implementation notes

In the definition of P.IsTriangulated, 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. the subtype of ObjectProperty C consisting of triangulated subcategories 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

class CategoryTheory.ObjectProperty.IsTriangulatedClosed₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

Given P : ObjectProperty C with C a pretriangulated category, this is the property that whenever X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ is a distinguished triangle such that P X₂ and P X₃ hold, then P.isoClosure X₁ holds.

• ext₁' (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → P T.obj₂ → P T.obj₃ → P.isoClosure T.obj₁

class CategoryTheory.ObjectProperty.IsTriangulatedClosed₂ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

Given P : ObjectProperty C with C a pretriangulated category, this is the property that whenever X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ is a distinguished triangle such that P X₁ and P X₃ hold, then P.isoClosure X₂ holds.

• ext₂' (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂

class CategoryTheory.ObjectProperty.IsTriangulatedClosed₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

Given P : ObjectProperty C with C a pretriangulated category, this is the property that whenever X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ is a distinguished triangle such that P X₁ and P X₂ hold, then P.isoClosure X₃ holds.

• ext₃' (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → P T.obj₁ → P T.obj₂ → P.isoClosure T.obj₃

theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₁] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₂ : P T.obj₂) (h₃ : P T.obj₃) : P.isoClosure T.obj₁

theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₂] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₃ : P T.obj₃) : P.isoClosure T.obj₂

theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₃] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P.isoClosure T.obj₃

theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₁] [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₂ : P T.obj₂) (h₃ : P T.obj₃) : P T.obj₁

theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₂] [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₃ : P T.obj₃) : P T.obj₂

theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₃] [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P T.obj₃

theorem CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsClosedUnderIsomorphisms] (hP : ∀ T ∈ Pretriangulated.distinguishedTriangles, P T.obj₂ → P T.obj₃ → P T.obj₁) : P.IsTriangulatedClosed₁

theorem CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsClosedUnderIsomorphisms] (hP : ∀ T ∈ Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂) : P.IsTriangulatedClosed₂

theorem CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsClosedUnderIsomorphisms] (hP : ∀ T ∈ Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₂ → P T.obj₃) : P.IsTriangulatedClosed₃

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂IsoClosure {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₂] : P.isoClosure.IsTriangulatedClosed₂

class CategoryTheory.ObjectProperty.IsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) extends P.ContainsZero, P.IsStableUnderShift ℤ, P.IsTriangulatedClosed₂ : Prop

The property that P : ObjectProperty C is a triangulated subcategory (of a pretriangulated category C).

• exists_zero : ∃ (Z : C), Limits.IsZero Z ∧ P Z
• isStableUnderShiftBy (a : ℤ) : P.IsStableUnderShiftBy a
• ext₂' (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₁OfIsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] : P.IsTriangulatedClosed₁

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₃OfIsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] : P.IsTriangulatedClosed₃

instance CategoryTheory.ObjectProperty.instIsTriangulatedIsoClosure {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] : P.isoClosure.IsTriangulated

def CategoryTheory.ObjectProperty.trW {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : MorphismProperty C

Given P : ObjectProperty C with C a pretriangulated category, this is the class of morphisms whose cone satisfies P. (The name trW contains the prefix tr for "triangulated", and W is a letter that is often used to refer to classes of morphisms with respect to which we may consider the localized category.)

Equations

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

theorem CategoryTheory.ObjectProperty.trW_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) : P.trW f ↔ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), P Z

theorem CategoryTheory.ObjectProperty.trW_iff' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] {Y Z : C} (g : Y ⟶ Z) : P.trW g ↔ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), P X

theorem CategoryTheory.ObjectProperty.trW.mk {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {T : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (h : P T.obj₃) : P.trW T.mor₁

theorem CategoryTheory.ObjectProperty.trW.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] {T : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (h : P T.obj₁) : P.trW T.mor₂

theorem CategoryTheory.ObjectProperty.trW_isoClosure {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.isoClosure.trW = P.trW

instance CategoryTheory.ObjectProperty.instRespectsIsoTrW {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.trW.RespectsIso

instance CategoryTheory.ObjectProperty.instContainsIdentitiesTrWOfContainsZero {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.ContainsZero] : P.trW.ContainsIdentities

theorem CategoryTheory.ObjectProperty.trW_of_isIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.ContainsZero] {X Y : C} (f : X ⟶ Y) [IsIso f] : P.trW f

theorem CategoryTheory.ObjectProperty.smul_mem_trW_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) (n : ℤˣ) : P.trW (n • f) ↔ P.trW f

theorem CategoryTheory.ObjectProperty.trW.shift {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} (hf : P.trW f) (n : ℤ) : P.trW ((shiftFunctor C n).map f)

theorem CategoryTheory.ObjectProperty.trW.unshift {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} {n : ℤ} (hf : P.trW ((shiftFunctor C n).map f)) : P.trW f

instance CategoryTheory.ObjectProperty.instIsCompatibleWithShiftTrWIntOfIsStableUnderShift {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] : P.trW.IsCompatibleWithShift ℤ

instance CategoryTheory.ObjectProperty.instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] [P.IsTriangulated] : P.trW.IsMultiplicative

theorem CategoryTheory.ObjectProperty.trW_iff_of_distinguished {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : P.trW T.mor₁ ↔ P T.obj₃

instance CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] [P.IsTriangulated] : P.trW.HasLeftCalculusOfFractions

instance CategoryTheory.ObjectProperty.instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] [P.IsTriangulated] : P.trW.HasRightCalculusOfFractions

instance CategoryTheory.ObjectProperty.instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] [P.IsTriangulated] : P.trW.IsCompatibleWithTriangulation

@[deprecated CategoryTheory.ObjectProperty.IsTriangulated (since := "2025-07-21")]

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

Alias of CategoryTheory.ObjectProperty.IsTriangulated.

---

The property that P : ObjectProperty C is a triangulated subcategory (of a pretriangulated category C).

Equations

• @CategoryTheory.Triangulated.Subcategory = @CategoryTheory.ObjectProperty.IsTriangulated

@[deprecated CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk' (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsClosedUnderIsomorphisms] (hP : ∀ T ∈ Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂) : P.IsTriangulatedClosed₂

Alias of CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk'.

@[deprecated CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁ (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.ext₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₁] [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₂ : P T.obj₂) (h₃ : P T.obj₃) : P T.obj₁

Alias of CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁.

@[deprecated CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁' (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.ext₁' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₁] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₂ : P T.obj₂) (h₃ : P T.obj₃) : P.isoClosure T.obj₁

Alias of CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁'.

@[deprecated CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂ (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.ext₂ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₂] [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₃ : P T.obj₃) : P T.obj₂

Alias of CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂.

@[deprecated CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂' (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.ext₂' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₂] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₃ : P T.obj₃) : P.isoClosure T.obj₂

Alias of CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂'.

@[deprecated CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃ (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.ext₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₃] [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P T.obj₃

Alias of CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃.

@[deprecated CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃' (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.ext₃' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₃] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P.isoClosure T.obj₃

Alias of CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃'.

@[deprecated CategoryTheory.ObjectProperty.trW (since := "2025-07-21")]

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

Alias of CategoryTheory.ObjectProperty.trW.

---

Given P : ObjectProperty C with C a pretriangulated category, this is the class of morphisms whose cone satisfies P. (The name trW contains the prefix tr for "triangulated", and W is a letter that is often used to refer to classes of morphisms with respect to which we may consider the localized category.)

Equations

• @CategoryTheory.Triangulated.Subcategory.W = @CategoryTheory.ObjectProperty.trW

@[deprecated CategoryTheory.ObjectProperty.trW_iff (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) : P.trW f ↔ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), P Z

Alias of CategoryTheory.ObjectProperty.trW_iff.

@[deprecated CategoryTheory.ObjectProperty.trW_iff' (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W_iff' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] {Y Z : C} (g : Y ⟶ Z) : P.trW g ↔ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), P X

Alias of CategoryTheory.ObjectProperty.trW_iff'.

@[deprecated CategoryTheory.ObjectProperty.trW.mk (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W.mk {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {T : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (h : P T.obj₃) : P.trW T.mor₁

Alias of CategoryTheory.ObjectProperty.trW.mk.

@[deprecated CategoryTheory.ObjectProperty.trW.mk' (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W.mk' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] {T : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (h : P T.obj₁) : P.trW T.mor₂

Alias of CategoryTheory.ObjectProperty.trW.mk'.

@[deprecated CategoryTheory.ObjectProperty.trW_isoClosure (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.isoClosure_W {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.isoClosure.trW = P.trW

Alias of CategoryTheory.ObjectProperty.trW_isoClosure.

@[deprecated CategoryTheory.ObjectProperty.trW_of_isIso (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W_of_isIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.ContainsZero] {X Y : C} (f : X ⟶ Y) [IsIso f] : P.trW f

Alias of CategoryTheory.ObjectProperty.trW_of_isIso.

@[deprecated CategoryTheory.ObjectProperty.smul_mem_trW_iff (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.smul_mem_W_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) (n : ℤˣ) : P.trW (n • f) ↔ P.trW f

Alias of CategoryTheory.ObjectProperty.smul_mem_trW_iff.

@[deprecated CategoryTheory.ObjectProperty.trW.shift (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W.shift {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} (hf : P.trW f) (n : ℤ) : P.trW ((shiftFunctor C n).map f)

Alias of CategoryTheory.ObjectProperty.trW.shift.

@[deprecated CategoryTheory.ObjectProperty.trW.unshift (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.W.unshift {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} {n : ℤ} (hf : P.trW ((shiftFunctor C n).map f)) : P.trW f

Alias of CategoryTheory.ObjectProperty.trW.unshift.

@[deprecated CategoryTheory.ObjectProperty.trW_iff_of_distinguished (since := "2025-07-21")]

theorem CategoryTheory.Triangulated.Subcategory.mem_W_iff_of_distinguished {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : P.trW T.mor₁ ↔ P T.obj₃

Alias of CategoryTheory.ObjectProperty.trW_iff_of_distinguished.