# Well-powered categories #

A category (C : Type u) [Category.{v} C] is [WellPowered C] if for every X : C, we have Small.{v} (Subobject X).

(Note that in this situation Subobject X : Type (max u v), so this is a nontrivial condition for large categories, but automatic for small categories.)

This is equivalent to the category MonoOver X being EssentiallySmall.{v} for all X : C.

When a category is well-powered, you can obtain nonconstructive witnesses as Shrink (Subobject X) : Type v and equivShrink (Subobject X) : Subobject X ≃ Shrink (subobject X).

class CategoryTheory.WellPowered (C : Type u₁) [] :

A category (with morphisms in Type v) is well-powered if Subobject X is v-small for every X.

We show in wellPowered_of_essentiallySmall_monoOver and essentiallySmall_monoOver that this is the case if and only if MonoOver X is v-essentially small for every X.

• subobject_small : ∀ (X : C),
Instances
theorem CategoryTheory.WellPowered.subobject_small {C : Type u₁} [] [self : ] (X : C) :
instance CategoryTheory.small_subobject (C : Type u₁) [] (X : C) :
Equations
• =
@[instance 100]
Equations
• =
theorem CategoryTheory.wellPowered_of_essentiallySmall_monoOver {C : Type u₁} [] (h : ∀ (X : C), ) :
instance CategoryTheory.essentiallySmall_monoOver {C : Type u₁} [] (X : C) :
Equations
• =
theorem CategoryTheory.wellPowered_of_equiv {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
theorem CategoryTheory.wellPowered_congr {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

Being well-powered is preserved by equivalences, as long as the two categories involved have their morphisms in the same universe.