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.

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

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

    Equations
    Instances For