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.
@[simp]
@[simp]
theorem
types.mono_over_equivalence_set_inverse_map
(α : Type u)
(s t : set α)
(b : s ⟶ t) :
(types.mono_over_equivalence_set α).inverse.map b = category_theory.mono_over.hom_mk (λ (w : (category_theory.mono_over.mk' subtype.val).obj.left), ⟨w.val, _⟩) _
The category of mono_over α
, for α : Type u
, is equivalent to the partial order set α
.
Equations
- types.mono_over_equivalence_set α = {functor := {obj := λ (f : category_theory.mono_over α), set.range f.obj.hom, map := λ (f g : category_theory.mono_over α) (t : f ⟶ g), category_theory.hom_of_le _, map_id' := _, map_comp' := _}, inverse := {obj := λ (s : set α), category_theory.mono_over.mk' subtype.val, map := λ (s t : set α) (b : s ⟶ t), category_theory.mono_over.hom_mk (λ (w : (category_theory.mono_over.mk' subtype.val).obj.left), ⟨w.val, _⟩) _, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components (λ (f : category_theory.mono_over α), category_theory.mono_over.iso_mk (equiv.of_injective f.obj.hom _).to_iso _) _, counit_iso := category_theory.nat_iso.of_components (λ (s : set α), category_theory.eq_to_iso subtype.range_val) _, functor_unit_iso_comp' := _}
@[simp]
theorem
types.mono_over_equivalence_set_functor_map
(α : Type u)
(f g : category_theory.mono_over α)
(t : f ⟶ g) :
@[simp]
theorem
types.mono_over_equivalence_set_functor_obj
(α : Type u)
(f : category_theory.mono_over α) :
@[simp]
@[simp]
@[protected, instance]
For α : Type u
, subobject α
is order isomorphic to set α
.