Subobjects satisfying a property of objects

Let P be a property of objects in a well-powered category with coproducts and images, so that Subobject X has arbitrary suprema, and with equalizers, so that the map onto the image of a morphism is an epimorphism. If P is closed under quotients and coproducts, then the supremum of any set of subobjects satisfying P again satisfies P. In particular, every object X has a greatest subobject satisfying P, namely Subobject.sSup {A | P A}.

theorem CategoryTheory.ObjectProperty.prop_subobjectSSup {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] [∀ (J : Type w), P.IsClosedUnderColimitsOfShape (Discrete J)] [LocallySmall.{w, v, u} C] [WellPowered.{w, v, u} C] [Limits.HasCoproducts C] [Limits.HasImages C] [Limits.HasEqualizers C] {X : C} (s : Set (Subobject X)) (hs : ∀ A ∈ s, P (Subobject.underlying.obj A)) : P (Subobject.underlying.obj (Subobject.sSup s))

If P is closed under quotients and coproducts, then the supremum of a set of subobjects satisfying P again satisfies P. In particular, together with Subobject.le_sSup, the subobject Subobject.sSup {A | P A} is the greatest subobject of X satisfying P.