Orthogonals are closed under extensions, and Dickson's theorem

In a preadditive balanced category, we show that both P.leftOrthogonal and P.rightOrthogonal are closed under extensions, using the kernel and cokernel supplied by a short exact sequence.

In a well-powered abelian category with coproducts, we show in ObjectProperty.leftOrthogonal_rightOrthogonal_eq_self that a property P which is closed under quotients, extensions, and coproducts satisfies P.rightOrthogonal.leftOrthogonal = P. This is the hard direction of S. E. Dickson's characterisation of torsion classes. The easy direction is assembled from the closure instances in Mathlib/CategoryTheory/ObjectProperty/OrthogonalLimits.lean.

References

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

Closure under extensions uses the kernel and cokernel supplied by a short exact sequence, so these two instances are stated for preadditive balanced categories.

instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsLeftOrthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] (P : ObjectProperty C) : P.leftOrthogonal.IsClosedUnderExtensions

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsRightOrthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] (P : ObjectProperty C) : P.rightOrthogonal.IsClosedUnderExtensions

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

The hard direction of Dickson's theorem: in a well-powered abelian category with coproducts, a property P closed under quotients, extensions, and coproducts is recovered as the left orthogonal of its right orthogonal.

theorem CategoryTheory.ObjectProperty.rightOrthogonal_cokernel_sSup {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] [P.IsClosedUnderExtensions] [∀ (J : Type w), P.IsClosedUnderColimitsOfShape (Discrete J)] [LocallySmall.{w, v, u} C] [WellPowered.{w, v, u} C] [Limits.HasCoproducts C] (X : C) : P.rightOrthogonal (Limits.cokernel (Subobject.sSup {A : Subobject X | P (Subobject.underlying.obj A)}).arrow)

In a well-powered abelian category with coproducts, if P is closed under quotients, extensions, and coproducts, then for any X, the cokernel of the arrow of the largest P-subobject of X satisfies P.rightOrthogonal.

theorem CategoryTheory.ObjectProperty.leftOrthogonal_rightOrthogonal_le {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] [P.IsClosedUnderExtensions] [∀ (J : Type w), P.IsClosedUnderColimitsOfShape (Discrete J)] [LocallySmall.{w, v, u} C] [WellPowered.{w, v, u} C] [Limits.HasCoproducts C] : P.rightOrthogonal.leftOrthogonal ≤ P

In a well-powered abelian category with coproducts, if P is closed under quotients, extensions, and coproducts, then P.rightOrthogonal.leftOrthogonal ≤ P. Together with ObjectProperty.le_leftOrthogonal_rightOrthogonal, this gives the equality ObjectProperty.leftOrthogonal_rightOrthogonal_eq_self.

theorem CategoryTheory.ObjectProperty.leftOrthogonal_rightOrthogonal_eq_self {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] [P.IsClosedUnderExtensions] [∀ (J : Type w), P.IsClosedUnderColimitsOfShape (Discrete J)] [LocallySmall.{w, v, u} C] [WellPowered.{w, v, u} C] [Limits.HasCoproducts C] : P.rightOrthogonal.leftOrthogonal = P

In a well-powered abelian category with coproducts, if P is closed under quotients, extensions, and coproducts, then P.rightOrthogonal.leftOrthogonal = P. This is the hard direction of S. E. Dickson's characterisation of torsion classes, see CategoryTheory.Abelian.isTorsionClass_iff.