Eventually orthogonal objects

Let C be a pretriangulated category and S : ℤ → ObjectProperty C a family of classes of objects. An object Y is eventually right orthogonal to S if it lies in the right orthogonal of S n for all n large enough, and eventually left orthogonal if it lies in the left orthogonal of S n for all n large enough.

Both classes are closed under isomorphisms and retracts, contain the zero objects, and are closed under extensions in distinguished triangles (IsTriangulatedClosed₂), since each right or left orthogonal is and finitely many bounds have a maximum. If shifting moves S n into S (n + c) for some c depending on the shift, they are also stable under shifts, hence triangulated subcategories.

A typical family is given by the objects of an abelian category placed in degree n (or -n) of its derived category: vanishing statements for morphisms to or from objects in sufficiently high (or low) degrees then pass from generators to the thick subcategory they generate.

Main definitions

• CategoryTheory.ObjectProperty.eventuallyRightOrthogonal: the objects in the right orthogonal of S n for all large n.
• CategoryTheory.ObjectProperty.eventuallyLeftOrthogonal: the objects in the left orthogonal of S n for all large n.

Main results

• CategoryTheory.ObjectProperty.isStableUnderShift_eventuallyRightOrthogonal and CategoryTheory.ObjectProperty.isStableUnderShift_eventuallyLeftOrthogonal: stability under shifts, when shifts move the family along its index.

def CategoryTheory.ObjectProperty.eventuallyRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ℤ → ObjectProperty C) : ObjectProperty C

The objects in the right orthogonal of S n for all n large enough.

def CategoryTheory.ObjectProperty.eventuallyLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (S : ℤ → ObjectProperty C) : ObjectProperty C

The objects in the left orthogonal of S n for all n large enough.

theorem CategoryTheory.ObjectProperty.eventuallyRightOrthogonal_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} {Y : C} : eventuallyRightOrthogonal S Y ↔ ∃ (n₀ : ℤ), ∀ n ≥ n₀, (S n).rightOrthogonal Y

An object is eventually right orthogonal to S if it is right orthogonal to S n for all large n.

theorem CategoryTheory.ObjectProperty.eventuallyLeftOrthogonal_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} {X : C} : eventuallyLeftOrthogonal S X ↔ ∃ (n₀ : ℤ), ∀ n ≥ n₀, (S n).leftOrthogonal X

An object is eventually left orthogonal to S if it is left orthogonal to S n for all large n.

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsEventuallyRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} : (eventuallyRightOrthogonal S).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsEventuallyLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} : (eventuallyLeftOrthogonal S).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsEventuallyRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} : (eventuallyRightOrthogonal S).IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsEventuallyLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} : (eventuallyLeftOrthogonal S).IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instContainsZeroEventuallyRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} [Limits.HasZeroObject C] : (eventuallyRightOrthogonal S).ContainsZero

instance CategoryTheory.ObjectProperty.instContainsZeroEventuallyLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} [Limits.HasZeroObject C] : (eventuallyLeftOrthogonal S).ContainsZero

theorem CategoryTheory.ObjectProperty.isStableUnderShift_eventuallyRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).PreservesZeroMorphisms] (hS : ∀ (a : ℤ), ∃ (c : ℤ), ∀ (n : ℤ) (X : C), S n X → S (n + c) (X⟦-a⟧)) : (eventuallyRightOrthogonal S).IsStableUnderShift ℤ

Shift stability of eventual right orthogonality: if shifting by -a moves S n into S (n + c) for some c, then the objects eventually right orthogonal to S are stable under shifts.

theorem CategoryTheory.ObjectProperty.isStableUnderShift_eventuallyLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {S : ℤ → ObjectProperty C} [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).PreservesZeroMorphisms] (hS : ∀ (a : ℤ), ∃ (c : ℤ), ∀ (n : ℤ) (Y : C), S n Y → S (n + c) (Y⟦-a⟧)) : (eventuallyLeftOrthogonal S).IsStableUnderShift ℤ

Shift stability of eventual left orthogonality: if shifting by -a moves S n into S (n + c) for some c, then the objects eventually left orthogonal to S are stable under shifts.

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂EventuallyRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {S : ℤ → ObjectProperty C} : (eventuallyRightOrthogonal S).IsTriangulatedClosed₂

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂EventuallyLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {S : ℤ → ObjectProperty C} : (eventuallyLeftOrthogonal S).IsTriangulatedClosed₂