Induced t-structures

Let t be a t-structure on a pretriangulated category C. If P is a triangulated subcategory of C, we introduce a typeclass P.HasInducedTStructure t which essentially says that up to isomorphisms P is stable by the application of the truncation functors.

In particular, we show that the triangulated subcategory t.plus of t-bounded above objects can be endowed with a t-structure t.onPlus, and the same applies to t.minus and t.bounded.

class CategoryTheory.ObjectProperty.HasInducedTStructure {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (t : Triangulated.TStructure C) [P.IsTriangulated] : Prop

The property that a full subcategory of a pretriangulated category equipped with a t-structure can be endowed with an induced t-structure.

• exists_triangle_zero_one (A : C) (hA : P A) : ∃ (X : C) (Y : C) (_ : t.IsLE X 0) (_ : t.IsGE Y 1) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), P.isoClosure X ∧ P.isoClosure Y

theorem CategoryTheory.ObjectProperty.hasInducedTStructure_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (t : Triangulated.TStructure C) [P.IsTriangulated] : P.HasInducedTStructure t ↔ ∀ (A : C), P A → ∃ (X : C) (Y : C) (_ : t.IsLE X 0) (_ : t.IsGE Y 1) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), P.isoClosure X ∧ P.isoClosure Y

noncomputable def CategoryTheory.ObjectProperty.tStructure {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (t : Triangulated.TStructure C) [P.IsTriangulated] [h : P.HasInducedTStructure t] : Triangulated.TStructure P.FullSubcategory

The t-structure induced on a full subcategory.

theorem CategoryTheory.ObjectProperty.tStructure_isLE_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (t : Triangulated.TStructure C) [P.IsTriangulated] [h : P.HasInducedTStructure t] (X : P.FullSubcategory) (n : ℤ) : (P.tStructure t).IsLE X n ↔ t.IsLE X.obj n

theorem CategoryTheory.ObjectProperty.tStructure_isGE_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (t : Triangulated.TStructure C) [P.IsTriangulated] [h : P.HasInducedTStructure t] (X : P.FullSubcategory) (n : ℤ) : (P.tStructure t).IsGE X n ↔ t.IsGE X.obj n

theorem CategoryTheory.ObjectProperty.HasInducedTStructure.mk' {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} [P.IsTriangulated] {t : Triangulated.TStructure C} (h : ∀ (X : C), P X → ∀ (n : ℤ), P ((t.truncLE n).obj X) ∧ P ((t.truncGE n).obj X)) : P.HasInducedTStructure t

Constructor for HasInducedTStructure.

theorem CategoryTheory.ObjectProperty.mem_of_hasInductedTStructure {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] (t : Triangulated.TStructure C) [P.IsClosedUnderIsomorphisms] [P.HasInducedTStructure t] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₁ : t.IsLE T.obj₁ n₀) (h₂ : P T.obj₂) (h₃ : t.IsGE T.obj₃ n₁) : P T.obj₁ ∧ P T.obj₃

instance CategoryTheory.ObjectProperty.instHasInducedTStructureMinOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P P' : ObjectProperty C) [P.IsTriangulated] [P'.IsTriangulated] (t : Triangulated.TStructure C) [P.HasInducedTStructure t] [P'.HasInducedTStructure t] [P.IsClosedUnderIsomorphisms] [P'.IsClosedUnderIsomorphisms] : (P ⊓ P').HasInducedTStructure t

instance CategoryTheory.Triangulated.TStructure.instHasInducedTStructurePlus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : t.plus.HasInducedTStructure t

instance CategoryTheory.Triangulated.TStructure.instHasInducedTStructureMinus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : t.minus.HasInducedTStructure t

instance CategoryTheory.Triangulated.TStructure.instHasInducedTStructureBounded {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : t.bounded.HasInducedTStructure t

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.onPlus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : TStructure t.plus.FullSubcategory

The t-structure induced on the full subcategory of t-bounded above objects.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.onMinus {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : TStructure t.minus.FullSubcategory

The t-structure induced on the full subcategory of t-bounded below objects.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.onBounded {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : TStructure t.bounded.FullSubcategory

The t-structure induced on the full subcategory of t-bounded objects.