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 (TypeCat.ofHom Subtype.val)

noncomputable def Types.monoOverEquivalenceSet (α : Type u) : CategoryTheory.MonoOver α ≌ Set α

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.

@[simp]

theorem Types.monoOverEquivalenceSet_inverse_map (α : Type u) {s t : Set α} (b : s ⟶ t) : (monoOverEquivalenceSet α).inverse.map b = CategoryTheory.MonoOver.homMk (TypeCat.ofHom fun (w : (CategoryTheory.MonoOver.mk (TypeCat.ofHom Subtype.val)).obj.left) => ⟨↑w, ⋯⟩) ⋯

@[simp]

theorem Types.monoOverEquivalenceSet_counitIso (α : Type u) : (monoOverEquivalenceSet α).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : Set α) => CategoryTheory.eqToIso ⋯) ⋯

@[simp]

theorem Types.monoOverEquivalenceSet_functor_map (α : Type u) {f g : CategoryTheory.MonoOver α} (t : f ⟶ g) : (monoOverEquivalenceSet α).functor.map t = CategoryTheory.homOfLE ⋯

@[simp]

theorem Types.monoOverEquivalenceSet_inverse_obj (α : Type u) (s : Set α) : (monoOverEquivalenceSet α).inverse.obj s = CategoryTheory.MonoOver.mk (TypeCat.ofHom Subtype.val)

@[simp]

theorem Types.monoOverEquivalenceSet_functor_obj (α : Type u) (f : CategoryTheory.MonoOver α) : (monoOverEquivalenceSet α).functor.obj f = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.obj.hom)

@[simp]

theorem Types.monoOverEquivalenceSet_unitIso (α : Type u) : (monoOverEquivalenceSet α).unitIso = CategoryTheory.NatIso.ofComponents (fun (f : CategoryTheory.MonoOver α) => CategoryTheory.MonoOver.isoMk (Equiv.ofInjective ⇑(CategoryTheory.ConcreteCategory.hom f.obj.hom) ⋯).toIso ⋯) ⋯

instance instWellPoweredType : CategoryTheory.WellPowered.{u, u, u + 1} (Type u)

noncomputable def Types.subobjectEquivSet (α : Type u) : CategoryTheory.Subobject α ≃o Set α

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

Equations

• Types.subobjectEquivSet α = (Types.monoOverEquivalenceSet α).thinSkeletonOrderIso