Well-powered categories

A category (C : Type u) [Category.{v} C] is [WellPowered.{w} C] if C is locally small relative to w and for every X : C, we have Small.{w} (Subobject X). The most common cases if when w = v, in which case, it only involves the condition 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.{w} for all X : C.

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

class CategoryTheory.WellPowered (C : Type u₁) [Category.{v, u₁} C] [LocallySmall.{w, v, u₁} C] : Prop

A category (with morphisms in Type v) is well-powered relative to a universe w if it is locally small and Subobject X is w-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 w-essentially small for every X.

• subobject_small (X : C) : Small.{w, max u₁ v} (Subobject X)

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

@[instance 100]

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

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

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

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

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

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

Being well-powered is preserved by equivalences.

instance CategoryTheory.instWellPoweredShrinkHoms {C : Type u₁} [Category.{v, u₁} C] [LocallySmall.{w, v, u₁} C] [WellPowered.{w, v, u₁} C] : WellPowered.{w, w, u₁} (ShrinkHoms.{u₁} C)