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.
theorem
subtype_val_mono
{α : Type u}
(s : Set α)
:
CategoryTheory.Mono (CategoryTheory.asHom Subtype.val)
@[simp]
theorem
Types.monoOverEquivalenceSet_inverse_map
(α : Type u)
{s : Set α}
{t : Set α}
(b : s ⟶ t)
:
(Types.monoOverEquivalenceSet α).inverse.map b = CategoryTheory.MonoOver.homMk
(fun (w : ((fun (s : Set α) => CategoryTheory.MonoOver.mk' Subtype.val) s).obj.left) => ⟨↑w, ⋯⟩) ⋯
@[simp]
theorem
Types.monoOverEquivalenceSet_unitIso
(α : Type u)
:
(Types.monoOverEquivalenceSet α).unitIso = CategoryTheory.NatIso.ofComponents
(fun (f : CategoryTheory.MonoOver α) => CategoryTheory.MonoOver.isoMk (Equiv.ofInjective f.obj.hom ⋯).toIso ⋯) ⋯
@[simp]
theorem
Types.monoOverEquivalenceSet_counitIso
(α : Type u)
:
(Types.monoOverEquivalenceSet α).counitIso = CategoryTheory.NatIso.ofComponents (fun (s : Set α) => CategoryTheory.eqToIso ⋯) ⋯
@[simp]
theorem
Types.monoOverEquivalenceSet_functor_map
(α : Type u)
{f : CategoryTheory.MonoOver α}
{g : CategoryTheory.MonoOver α}
(t : f ⟶ g)
:
(Types.monoOverEquivalenceSet α).functor.map t = CategoryTheory.homOfLE ⋯
@[simp]
theorem
Types.monoOverEquivalenceSet_inverse_obj
(α : Type u)
(s : Set α)
:
(Types.monoOverEquivalenceSet α).inverse.obj s = CategoryTheory.MonoOver.mk' Subtype.val
@[simp]
theorem
Types.monoOverEquivalenceSet_functor_obj
(α : Type u)
(f : CategoryTheory.MonoOver α)
:
(Types.monoOverEquivalenceSet α).functor.obj f = Set.range f.obj.hom
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
Equations
For α : Type u
, Subobject α
is order isomorphic to Set α
.
Equations
- Types.subobjectEquivSet α = (Types.monoOverEquivalenceSet α).thinSkeletonOrderIso