# mathlib3documentation

category_theory.subobject.well_powered

# Well-powered categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A category (C : Type u) [category.{v} C] is [well_powered C] if for every X : C, we have small.{v} (subobject X).

(Note that in this situtation 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 mono_over X being essentially_small.{v} for all X : C.

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

@[class]
structure category_theory.well_powered (C : Type u₁)  :
Prop
• subobject_small : ( (X : C), . "apply_instance"

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

We show in well_powered_of_mono_over_essentially_small and mono_over_essentially_small that this is the case if and only if mono_over X is v-essentially small for every X.

Instances of this typeclass
@[protected, instance]
def category_theory.small_subobject (C : Type u₁) (X : C) :
@[protected, instance]
@[protected, instance]
theorem category_theory.well_powered_of_equiv {C : Type u₁} {D : Type u₂} (e : C D)  :
theorem category_theory.well_powered_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.