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

source

@[class]

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

Prop

subobject_small : (∀ (X : C), small (category_theory.subobject X)) . "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

source

@[protected, instance]

def category_theory.small_subobject (C : Type u₁) [category_theory.category C] [category_theory.well_powered C] (X : C) :

small (category_theory.subobject X)

source

@[protected, instance]

def category_theory.well_powered_of_small_category (C : Type u₁) [category_theory.small_category C] :

category_theory.well_powered C

source

theorem category_theory.essentially_small_mono_over_iff_small_subobject {C : Type u₁} [category_theory.category C] (X : C) :

category_theory.essentially_small (category_theory.mono_over X) ↔ small (category_theory.subobject X)

source

theorem category_theory.well_powered_of_essentially_small_mono_over {C : Type u₁} [category_theory.category C] (h : ∀ (X : C), category_theory.essentially_small (category_theory.mono_over X)) :

category_theory.well_powered C

source

@[protected, instance]

def category_theory.essentially_small_mono_over {C : Type u₁} [category_theory.category C] [category_theory.well_powered C] (X : C) :

category_theory.essentially_small (category_theory.mono_over X)

source

theorem category_theory.well_powered_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) [category_theory.well_powered C] :

category_theory.well_powered D

source

theorem category_theory.well_powered_congr {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.well_powered C ↔ category_theory.well_powered D

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