Documentation

Mathlib.CategoryTheory.Subobject.Types

Type u is well-powered #

By building a categorical equivalence MonoOver α ≌ 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 [WellPowered 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.

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    For α : Type u, Subobject α is order isomorphic to Set α.

    Equations
    Instances For