# mathlibdocumentation

category_theory.subobject.types

# Type u is well-powered #

By building a categorical equivalence mono_over α ≌ set α for any α : Type u, we deduce that subobject α ≃o set α and that Type u is well-powered.

One would hope that for a particular concrete category C (AddCommGroup, etc) it's viable to prove [well_powered C] without explicitly aligning subobject X with the "hand-rolled" definition of subobjects.

This may be possible using Lawvere theories, but it remains to be seen whether this just pushes lumps around in the carpet.

theorem subtype_val_mono {α : Type u} (s : set α) :
@[simp]
@[simp]
theorem types.mono_over_equivalence_set_inverse_map (α : Type u) (s t : set α) (b : s t) :
def types.mono_over_equivalence_set (α : Type u) :

The category of mono_over α, for α : Type u, is equivalent to the partial order set α.

Equations
@[simp]
theorem types.mono_over_equivalence_set_functor_map (α : Type u) (f g : category_theory.mono_over α) (t : f g) :
@[simp]
@[simp]
theorem types.mono_over_equivalence_set_unit_iso (α : Type u) :
@[simp]
theorem types.mono_over_equivalence_set_inverse_obj (α : Type u) (s : set α) :
@[instance]
def types.subobject_equiv_set (α : Type u) :

For α : Type u, subobject α is order isomorphic to set α.

Equations