Retracts and canonical boundedness in triangulated categories #
This file contains t-structure facts that require no geometric input. In particular, the aisle, coaisle, and bounded object properties of an arbitrary t-structure are stable under retracts.
theorem
CategoryTheory.tStructureIsLE_of_retract
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : Triangulated.TStructure C)
{X Y : C}
(r : Retract X Y)
(n : ℤ)
(hY : t.IsLE Y n)
:
t.IsLE X n
The ≤ n part of a t-structure is stable under retracts.
theorem
CategoryTheory.tStructureIsGE_of_retract
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : Triangulated.TStructure C)
{X Y : C}
(r : Retract X Y)
(n : ℤ)
(hY : t.IsGE Y n)
:
t.IsGE X n
The ≥ n part of a t-structure is stable under retracts.
instance
CategoryTheory.instIsStableUnderRetractsMinus_derivedAlgGeo
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : Triangulated.TStructure C)
:
instance
CategoryTheory.instIsStableUnderRetractsPlus_derivedAlgGeo
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : Triangulated.TStructure C)
:
instance
CategoryTheory.instIsStableUnderRetractsBounded_derivedAlgGeo
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : Triangulated.TStructure C)
: