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₁) [CategoryTheory.Category.{v, u₁} C] : Prop

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) : Small.{v, max u₁ v} (CategoryTheory.Subobject X)

instance CategoryTheory.small_subobject (C : Type u₁) [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.WellPowered C] (X : C) : Small.{v, max u₁ v} (CategoryTheory.Subobject X)

@[instance 100]

instance CategoryTheory.wellPowered_of_smallCategory (C : Type u₁) [CategoryTheory.SmallCategory C] : CategoryTheory.WellPowered C

theorem CategoryTheory.essentiallySmall_monoOver_iff_small_subobject {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (X : C) : CategoryTheory.EssentiallySmall.{v, v, max u₁ v} (CategoryTheory.MonoOver X) ↔ Small.{v, max u₁ v} (CategoryTheory.Subobject X)

theorem CategoryTheory.wellPowered_of_essentiallySmall_monoOver {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (h : ∀ (X : C), CategoryTheory.EssentiallySmall.{v, v, max u₁ v} (CategoryTheory.MonoOver X)) : CategoryTheory.WellPowered C

instance CategoryTheory.essentiallySmall_monoOver {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.WellPowered C] (X : C) : CategoryTheory.EssentiallySmall.{v, v, max u₁ v} (CategoryTheory.MonoOver X)

theorem CategoryTheory.wellPowered_of_equiv {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (e : C ≌ D) [CategoryTheory.WellPowered C] : CategoryTheory.WellPowered D

theorem CategoryTheory.wellPowered_congr {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (e : C ≌ D) : CategoryTheory.WellPowered C ↔ CategoryTheory.WellPowered D

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