Orthogonal of triangulated subcategories

Let P be a triangulated subcategory of a pretriangulated category C. We show that P.rightOrthogonal (which consists of objects Y with no nonzero map X ⟶ Y with X satisfying P) is a triangulated subcategory. The dual result for P.leftOrthogonal is also obtained.

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftRightOrthogonal {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {M : Type u_1} [AddGroup M] [HasShift C M] [Limits.HasZeroMorphisms C] [P.IsStableUnderShift M] : P.rightOrthogonal.IsStableUnderShift M

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftLeftOrthogonal {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {M : Type u_1} [AddGroup M] [HasShift C M] [Limits.HasZeroMorphisms C] [P.IsStableUnderShift M] : P.leftOrthogonal.IsStableUnderShift M

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

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

instance CategoryTheory.ObjectProperty.instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [P.IsStableUnderShift ℤ] : P.rightOrthogonal.IsTriangulated

instance CategoryTheory.ObjectProperty.instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [P.IsStableUnderShift ℤ] : P.leftOrthogonal.IsTriangulated

theorem CategoryTheory.ObjectProperty.isLocal_trW {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [P.IsTriangulated] : P.trW.isLocal = P.rightOrthogonal

theorem CategoryTheory.ObjectProperty.isColocal_trW {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [P.IsTriangulated] : P.trW.isColocal = P.leftOrthogonal

theorem CategoryTheory.ObjectProperty.rightOrthogonal.map_bijective_of_isTriangulated {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [P.IsTriangulated] [IsTriangulated C] {Y : C} (hY : P.rightOrthogonal Y) (L : Functor C D) [L.IsLocalization P.trW] (X : C) : Function.Bijective L.map

theorem CategoryTheory.ObjectProperty.leftOrthogonal.map_bijective_of_isTriangulated {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [P.IsTriangulated] [IsTriangulated C] {X : C} (hX : P.leftOrthogonal X) (L : Functor C D) [L.IsLocalization P.trW] (Y : C) : Function.Bijective L.map