Orthogonals are closed under (co)limits, quotients and subobjects

Let P be a property of objects in a category with zero morphisms. We show that the left orthogonal P.leftOrthogonal is closed under quotients and under colimits of any shape, and, dually, that the right orthogonal P.rightOrthogonal is closed under subobjects and under limits of any shape.

These are registered as instances of IsClosedUnderQuotients, IsClosedUnderColimitsOfShape, IsClosedUnderSubobjects and IsClosedUnderLimitsOfShape. Closure of the orthogonals under extensions is shown in Mathlib/CategoryTheory/Abelian/OrthogonalClosed.lean; together these form the easy direction of S. E. Dickson's characterisation of torsion classes, see CategoryTheory.Abelian.isTorsionClass_iff.

References

• S. E. Dickson, A torsion theory for Abelian categories

instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.leftOrthogonal.IsClosedUnderQuotients

The left orthogonal of a property of objects is closed under quotients.

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) {J : Type u'} [Category.{v', u'} J] : P.leftOrthogonal.IsClosedUnderColimitsOfShape J

The left orthogonal of a property of objects is closed under colimits of any shape.

instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.rightOrthogonal.IsClosedUnderSubobjects

The right orthogonal of a property of objects is closed under subobjects.

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) {J : Type u'} [Category.{v', u'} J] : P.rightOrthogonal.IsClosedUnderLimitsOfShape J

The right orthogonal of a property of objects is closed under limits of any shape.