Skeleton of a category #
Define skeletal categories as categories in which any two isomorphic objects are equal.
Construct the skeleton of an arbitrary category by taking isomorphism classes, and show it is a skeleton of the original category.
In addition, construct the skeleton of a thin category as a partial ordering, and (noncomputably) show it is a skeleton of the original category. The advantage of this special case being handled separately is that lemmas and definitions about orderings can be used directly, for example for the subobject lattice. In addition, some of the commutative diagrams about the functors commute definitionally on the nose which is convenient in practice.
A category is skeletal if isomorphic objects are equal.
Equations
- CategoryTheory.Skeletal C = ∀ ⦃X Y : C⦄, CategoryTheory.IsIsomorphic X Y → X = Y
IsSkeletonOf C D F
says that F : D ⥤ C
exhibits D
as a skeletal full subcategory of C
,
in particular F
is a (strong) equivalence and D
is skeletal.
- skel : CategoryTheory.Skeletal D
The category
D
has isomorphic objects equal - eqv : F.IsEquivalence
The functor
F
is an equivalence
The category D
has isomorphic objects equal
The functor F
is an equivalence
If C
is thin and skeletal, then any naturally isomorphic functors to C
are equal.
If C
is thin and skeletal, D ⥤ C
is skeletal.
CategoryTheory.functor_thin
shows it is thin also.
Construct the skeleton category as the induced category on the isomorphism classes, and derive its category structure.
Equations
- CategoryTheory.Skeleton C = CategoryTheory.InducedCategory C Quotient.out
Equations
- CategoryTheory.instInhabitedSkeleton C = { default := ⟦default⟧ }
Equations
The functor from the skeleton of C
to C
.
Equations
- CategoryTheory.fromSkeleton C = CategoryTheory.inducedFunctor Quotient.out
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The equivalence between the skeleton and the category itself.
Equations
- CategoryTheory.skeletonEquivalence C = (CategoryTheory.fromSkeleton C).asEquivalence
The skeleton
of C
given by choice is a skeleton of C
.
Two categories which are categorically equivalent have skeletons with equivalent objects.
Equations
- One or more equations did not get rendered due to their size.
Construct the skeleton category by taking the quotient of objects. This construction gives a
preorder with nice definitional properties, but is only really appropriate for thin categories.
If your original category is not thin, you probably want to be using skeleton
instead of this.
Equations
Equations
- CategoryTheory.inhabitedThinSkeleton C = { default := Quotient.mk' default }
Equations
The functor from a category to its thin skeleton.
Equations
- CategoryTheory.toThinSkeleton C = { obj := Quotient.mk', map := fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
The constructions here are intended to be used when the category C
is thin, even though
some of the statements can be shown without this assumption.
The thin skeleton is thin.
Equations
- ⋯ = ⋯
A functor C ⥤ D
computably lowers to a functor ThinSkeleton C ⥤ ThinSkeleton D
.
Equations
- One or more equations did not get rendered due to their size.
Given a natural transformation F₁ ⟶ F₂
, induce a natural transformation map F₁ ⟶ map F₂
.
Equations
- One or more equations did not get rendered due to their size.
Given a bifunctor, we descend to a function on objects of ThinSkeleton
Equations
- CategoryTheory.ThinSkeleton.map₂ObjMap F x y = Quotient.map₂ (fun (X : C) (Y : D) => (F.obj X).obj Y) ⋯ x y
For each x : ThinSkeleton C
, we promote map₂ObjMap F x
to a functor
Equations
- One or more equations did not get rendered due to their size.
This provides natural transformations map₂Functor F x₁ ⟶ map₂Functor F x₂
given
x₁ ⟶ x₂
Equations
- One or more equations did not get rendered due to their size.
A functor C ⥤ D ⥤ E
computably lowers to a functor
ThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Use Quotient.out
to create a functor out of the thin skeleton.
Equations
- One or more equations did not get rendered due to their size.
The equivalence between the thin skeleton and the category itself.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- CategoryTheory.ThinSkeleton.thinSkeletonPartialOrder = PartialOrder.mk ⋯
fromThinSkeleton C
exhibits the thin skeleton as a skeleton.
Equations
- CategoryTheory.ThinSkeleton.isSkeletonOfInhabited = { default := ⋯ }
An adjunction between thin categories gives an adjunction between their thin skeletons.
Equations
- One or more equations did not get rendered due to their size.
When e : C ≌ α
is a categorical equivalence from a thin category C
to some partial order α
,
the ThinSkeleton C
is order isomorphic to α
.
Equations
- e.thinSkeletonOrderIso = ((CategoryTheory.ThinSkeleton.equivalence C).trans e).toOrderIso