mathlib documentation


Well-powered categories #

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).

structure category_theory.well_powered (C : Type u₁) [category_theory.category C] :

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

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