nLab skeleton



Category theory

Equality and Equivalence

This entry is about the notion of skeleton in category theory. For the notion of (co)skeletal simplicial sets see at simplicial skeleton.



A strict category π’ž\mathcal{C} is called skeletal if any two objects that are isomorphic are actually already equal (in the fixed set of objects Obj(π’ž)Obj(\mathcal{C})), hence if all its isomorphisms are automorphisms.

(If in addition all isomorphisms are in fact identity morphisms, then one speaks of a gaunt category. In the other extreme, if all morphisms of a skeletal category are isomorphisms, then one has a skeletal groupoid).

A skeleton of a category CC is defined to be a skeletal subcategory of CC whose inclusion functor exhibits it as equivalent to CC. A weak skeleton of CC is any skeletal category which is weakly equivalent to CC.

In the absence of the axiom of choice, it is more appropriate to define a skeleton of CC to be a weak skeleton as defined above.


In this section, we work in set-level foundations to construct skeleta of categories and more general objects.

Existence of Skeletons of Categories


If the axiom of choice holds, then every category CC has a skeleton (in the strongest sense).


Simply choose one object in each isomorphism class and one isomorphism to that object from each other object in that class.

In more detail, generate the full subcategory sk(C)sk(C) containing just the chosen objects. Denote by in:sk(C)β†’Cin\colon sk(C)\to C the inclusion. We exhibit a weak inverse of inin as a functor βˆ’β€²:x↦xβ€²-':x\mapsto x' constructed as follows. For every object xx one has chosen already the unique object xβ€²x' in sk(X)sk(X) isomorphic to xx, but one also needs to make a choice of isomorphism i x:xβ†’xβ€²i_x\colon x\to x' for every xx. This enables to conjugate between C(x,y)C(x,y) and C(xβ€²,yβ€²)C(x',y') by

(xβ†’fy)↦(xβ€²β†’i x βˆ’1xβ†’fyβ†’i yyβ€²). (x\stackrel{f}\to y)\mapsto (x'\stackrel{i_x^{-1}}\to x\stackrel{f}\to y\stackrel{i_y}\to y').

The rule for morphisms βˆ’β€²:f↦fβ€²:=i y∘f∘i x βˆ’1-': f\mapsto f' := i_y\circ f\circ i_{x}^{-1} is clearly functorial. Let us show that βˆ’β€²-' is a weak inverse of inin. In one direction, given y∈sk(C)y\in sk(C) we compute (in y)β€²=y(in_{y})' = y (strict equality); in another direction, given x∈Cx\in C, notice that i in xβ€² βˆ’1:in xβ€²β‰…xi^{-1}_{in_{x'}}:in_{x'}\cong x for x∈Cx\in C is an isomorphism. It suffices to show that these isomorphisms for all x∈Cx\in C together form a natural isomorphism i in βˆ’1:in βˆ’β€²β†’id Ci^{-1}_{in}:in_{-'}\to id_C; the naturality diagram is commutative precisely because of the conjugation formula for the functor βˆ’β€²-' for morphisms. This completes the proof that βˆ’β€²-' is indeed a weak inverse of inin.

In fact, the statement that every (possibly small) category has a skeleton is equivalent to the axiom of choice if β€œsubcategory” and β€œequivalence” have their naive (β€˜strong’) meanings. For given a surjection p:Aβ†’Bp:A\to B in SetSet, make AA into a category with a unique isomorphism aβ‰…aβ€²a\cong a' iff p(a)=p(aβ€²)p(a)=p(a'); then a skeleton of AA supplies a splitting of pp.

Even with the more general notion of weak or ana-equivalence of categories, some amount of choice is required to show that every category has a skeleton. It would be interesting to know the precise strength of the statement β€œevery category is weakly equivalent to a skeletal one.”

Skeletons as an Endo-Pseudofunctor on β„­π”žπ”±\mathfrak{Cat}

In the presence of choice we can thusly turn the process of taking the skeleton of a category into an endo-pseudofunctor on β„­π”žπ”±\mathfrak{Cat}, the 22-category of categories.

For each category π’ž\mathcal{C} let sk π’žsk_\mathcal{C} denote a skeleton of π’ž\mathcal{C} and let E π’ž:sk π’žβ‰ƒπ’ž:E π’ž ∼1E_\mathcal{C}:sk_\mathcal{C}\simeq\mathcal{C}:E_\mathcal{C}^{\sim1} denote the skeletal equivalence at π’ž\mathcal{C}, with Ο΅ π’ž sk:E π’žβˆ˜E π’ž ∼1β‡’1 π’ž\epsilon^{sk}_\mathcal{C}:E_\mathcal{C}\circ E^{\sim1}_\mathcal{C}\Rightarrow1_\mathcal{C} the skeletal transformation at π’ž\mathcal{C}. We define an endo-pseudofunctor

sk:β„­π”žπ”±β†’β„­π”žπ”± sk:\mathfrak{Cat}\to\mathfrak{Cat}

as follows:

  1. sk(π’ž)=sk π’ž,sk(\mathcal{C})=sk_\mathcal{C},
  2. sk(F:π’žβ†’π’Ÿ)=E π’Ÿ ∼1∘F∘E π’ž:sk π’žβ†’π’žβ†’π’Ÿβ†’sk π’Ÿ,sk(F:\mathcal{C}\to\mathcal{D})=E^{\sim1}_\mathcal{D}\circ F\circ E_\mathcal{C}:sk_\mathcal{C}\to\mathcal{C}\to\mathcal{D}\to sk_\mathcal{D},
  3. sk(Ξ±:Fβ‡’G)=i∘α∘i βˆ’1:sk(F)β‡’sk(G),sk(\alpha:F\Rightarrow G)=i\circ\alpha\circ i^{-1}:sk(F)\Rightarrow sk(G), where
    i∘α∘i βˆ’1:sk(F)β‡’sk(G) i\circ\alpha\circ i^{-1}:sk(F)\Rightarrow sk(G)

    is defined by

    (i∘α∘i βˆ’1) X=i G(X)∘α X∘i F(X) βˆ’1:F(X)β€²β†’F(X)β†’G(X)β†’G(X)β€². (i\circ\alpha\circ i^{-1})_X=i_{G(X)}\circ\alpha_X\circ i_{F(X)}^{-1}:F(X)'\to F(X)\to G(X)\to G(X)'.
  4. For each category π’ž\mathcal{C}, the unitor ΞΉ π’ž sk:1 sk(π’ž)β‡’sk(1 π’ž)\iota^{sk}_\mathcal{C}:1_{sk(\mathcal{C})}\Rightarrow sk(1_\mathcal{C}) is defined by
    ΞΉ π’ž sk=1 1 sk(π’ž), \iota^{sk}_\mathcal{C}=1_{1_{sk(\mathcal{C})}},


    sk(1 π’ž)=E π’ž ∼1∘1 π’žβˆ˜E π’ž=E π’ž ∼1∘E π’ž=1 sk(π’ž).sk(1_\mathcal{C})=E^{\sim1}_\mathcal{C}\circ1_\mathcal{C}\circ E_\mathcal{C}=E^{\sim1}_\mathcal{C}\circ E_\mathcal{C}=1_{sk(\mathcal{C})}.
  5. For each pair of composable functors F:π’žβ†’π’ŸF:\mathcal{C}\to\mathcal{D}, G:β„¬β†’π’žG:\mathcal{B}\to\mathcal{C}, the associator Ξ± F,G sk:sk(F)∘sk(G)β‡’sk(F∘G)\alpha^{sk}_{F,G}:sk(F)\circ sk(G)\Rightarrow sk(F\circ G) is defined by
    Ξ± F,G sk=1 E π’Ÿ ∼1∘F⋆ϡ π’ž sk⋆1 G∘E ℬ:E π’Ÿ ∼1∘F∘E π’žβˆ˜E π’ž ∼1∘G∘E ℬ⇒E π’Ÿ ∼1∘F∘G∘E ℬ. \alpha^{sk}_{F,G}=1_{E^{\sim1}_\mathcal{D}\circ F}\star\epsilon^{sk}_\mathcal{C}\star1_{G\circ E_\mathcal{B}}:E^{\sim1}_\mathcal{D}\circ F\circ E_\mathcal{C}\circ E_\mathcal{C}^{\sim1}\circ G\circ E_\mathcal{B}\Rightarrow E^{\sim1}_\mathcal{D}\circ F\circ G\circ E_\mathcal{B}.

Skeleton of an Indexed Category

Using the above definition, we can canonically define the skeleton of an indexed category.

Let ψ:ℬ opβ†’β„­π”žπ”±\psi:\mathcal{B}^{op}\to\mathfrak{Cat} be an indexed category. We define the indexed skeleton of ψ\psi, denoted

sk(ψ):ℬ opβ†’β„­π”žπ”±, sk(\psi):\mathcal{B}^{op}\to\mathfrak{Cat},

to be the indexed category given by postcomposing ψ\psi with sksk, so sk(ψ)=sk∘ψ.sk(\psi)=sk\circ\psi. That is, for each Iβˆˆβ„¬I\in\mathcal{B} we take a skeleton sk(ψ(I))sk(\psi(I)) of the category ψ(I)\psi(I) indexed by II with equivalence E I:ψ(I)≃sk(ψ(I)):E I ∼1E_I:\psi(I)\simeq sk(\psi(I)):E_I^{\sim1}, we extend functors using the equivalences at various skeletons, and we extend natural transformations using skeletal isomorphisms in the codomain categories (although ℬ op\mathcal{B}^{op} has only identity 22-cells since it’s a promoted 11-category, so the action on 22-cells is trivial).

Skeleton of a Fibered Category

Using the above definition and the Grothendieck construction, we can define the skeleton of a fibration using the skeleton of an indexed category.

Let p:ℰ→ℬp:\mathcal{E}\to\mathcal{B} be a fibration. We define the fibered skeleton of pp, denoted

sk(p):sk β„° p→ℬ sk(p):sk^p_\mathcal{E}\to\mathcal{B}

to be the Grothendieck completion of the indexed skeleton of the indexing by pp. That is, sk(p)sk(p) is the fibration obtained by turning pp into an indexed category using the Grothendieck construction, taking the indexed skeleton of this indexed category, then turning the resulting skeletal indexed category back into a fibration (via the Grothendieck construction again). We refer to the total category sk β„° psk^p_\mathcal{E} in the resulting fibration as the pp-skeleton of β„°\mathcal{E}, which is different than sk β„°sk_\mathcal{E} since we have only skeletalized the fiber categories of our original fibration and not the total category of the original fibration. In general, we will have that

sk ℰ≇sk β„° p, sk_\mathcal{E}\ncong sk^p_\mathcal{E},

although they are trivially equivalent. As an example of this construction in action, we can pass from the monomorphism fibration on a category with pullbacks to the subobject fibration by taking the fibered skeleton. For details, see the subobject fibration section of codomain fibration.


In this section we collect some properties of skeleta in set-level foundations.


Of course, two categories can be equivalent even if one is skeletal and the other is not. Thus, the notion of skeletal category violates the principle of equivalence. (It doesn’t make sense to ask whether a particular category, skeletal or not, β€œviolates the principle of equivalence”.)

Skeletons without Choice

Without any choice, we have the following theorems.


Any thin category (i.e. any preordered set) has a weak skeleton.


In this case, we can take the objects of the skeleton of CC to be the isomorphism classes of CC. If CC is thin, then we can define a partial ordering on its set of isomorphism classes, making them into a skeleton of CC.


Any two skeletons (in the strong sense) of a category are isomorphic.


Let π’ž\mathcal{C} be a category, with sk(π’ž)sk (\mathcal{C}) and sk(π’ž)β€²sk (\mathcal{C})' two skeletons of π’ž\mathcal{C}, and for each object Yβˆˆπ’žY\in\mathcal{C} denote by X YX_Y and X Yβ€²X_Y' respectively the unique objects in sk(π’ž)sk (\mathcal{C}) and sk(π’ž)β€²sk (\mathcal{C})' which are isomorphic to Y, and denote their respective isomorphisms by i Y:Yβ†’X Yi_Y:Y\to X_Y and i Yβ€²:Yβ†’X Yβ€²i_Y':Y\to X_Y'. We define a functor F:sk(π’ž)β†’sk(π’ž)β€²F:sk (\mathcal{C})\to sk (\mathcal{C})' by

F(X Y)=X Yβ€², F(X_Y)=X_Y',
F(f:X Yβ†’X Z)=i Zβ€²βˆ˜i Z βˆ’1∘f∘i Y∘i Yβ€² βˆ’1:X Yβ€²β†’Yβ†’X Yβ†’X Zβ†’Zβ†’X Zβ€². F(f:X_Y\to X_Z)=i_Z'\circ i_Z^{-1}\circ f\circ i_Y\circ i_Y'^{-1}:X_Y'\to Y\to X_Y\to X_Z\to Z\to X_Z'.

We then have

F(1 X Y)=i Yβ€²βˆ˜i Y βˆ’1∘1 X Y∘i Y∘i Yβ€² βˆ’1=i Yβ€²βˆ˜i Y βˆ’1∘i Y∘i Yβ€² βˆ’1=i Yβ€²βˆ˜1 Y∘i Yβ€² βˆ’1=i Yβ€²βˆ˜i Yβ€² βˆ’1=1 X Yβ€²=1 F(X Y), F(1_{X_Y})=i_Y'\circ i_Y^{-1}\circ 1_{X_Y}\circ i_Y\circ i_Y'^{-1}=i_Y'\circ i_Y^{-1}\circ i_Y\circ i_Y'^{-1}=i_Y'\circ1_Y\circ i_Y'^{-1}=i_Y'\circ i_Y'^{-1}=1_{X_Y'}=1_{F(X_Y)},
F(f:X Bβ†’X C)∘F(g:X Aβ†’X B)=i Cβ€²βˆ˜i C βˆ’1∘f∘i B∘i Bβ€² βˆ’1∘i Bβ€²βˆ˜i B βˆ’1∘g∘i A∘i Aβ€² βˆ’1 F(f:X_B\to X_C)\circ F(g:X_A\to X_B)=i_C'\circ i_C^{-1}\circ f\circ i_B\circ i_B'^{-1}\circ i_B'\circ i_B^{-1}\circ g\circ i_A\circ i_A'^{-1}
=i Cβ€²βˆ˜i C βˆ’1∘f∘i B∘1 B∘i B βˆ’1∘g∘i A∘i Aβ€² βˆ’1=i Cβ€²βˆ˜i C βˆ’1∘f∘i B∘i B βˆ’1∘g∘i A∘i Aβ€² βˆ’1 =i_C'\circ i_C^{-1}\circ f\circ i_B\circ 1_{B}\circ i_B^{-1}\circ g\circ i_A\circ i_A'^{-1}=i_C'\circ i_C^{-1}\circ f\circ i_B\circ i_B^{-1}\circ g\circ i_A\circ i_A'^{-1}
=i Cβ€²βˆ˜i C βˆ’1∘f∘1 X B∘g∘i A∘i Aβ€² βˆ’1=i Cβ€²βˆ˜i C βˆ’1∘f∘g∘i A∘i Aβ€² βˆ’1=F(f∘g), =i_C'\circ i_C^{-1}\circ f\circ1_{X_B}\circ g\circ i_A\circ i_A'^{-1}=i_C'\circ i_C^{-1}\circ f\circ g\circ i_A\circ i_A'^{-1}=F(f\circ g),

so FF is a functor. The inverse F βˆ’1:sk(π’ž)β€²β†’sk(π’ž)F^{-1}: sk (\mathcal{C})'\to sk (\mathcal{C}) is defined in the obvious way, and is functorial by similar computations.

Notice that the axiom of choice fails in general when one considers internal categories. Hence not every internal category has a skeleton. A necessary condition for an internal category X 1⇉X 0X_1 \rightrightarrows X_0 to have a skeleton is the existence quotient X 0/X 1X_0/X_1 - the object of orbits under the action of the core of XX. If the quotient map X 0β†’X 0/X 1X_0 \to X_0/X_1 has a section, then one could consider XX to have a skeleton, but this condition isn’t sufficient for the induced inclusion functor to be a weak equivalence of internal categories when this makes sense (i.e. if the category is internal to a site).

David Roberts: The claim above about the necessity of the existence of the quotient needs to be checked.

Equivalents of Choice

Define a coskeleton of a category CC to be a skeletal category SS with a surjective equivalence C→SC\to S. In Categories, Allegories it is shown that the following are equivalent.

  1. The axiom of choice holds.
  2. Any two ana-equivalent categories are strongly equivalent.
  3. Any two weakly equivalent categories are strongly equivalent.
  4. Every small category has a weak skeleton.
  5. Every small category has a coskeleton.
  6. Any two weak skeletons of a given small category are isomorphic.
  7. Any two coskeletons of a given small category are isomorphic.

For convenience we add:

  1. Given an inhabited family {S i} I\{S_i\}_I of equinumerous sets there exists 0∈I0 \in I and a family of isomorphisms of the permutation groups {Aut(S 0)β†’Aut(S i)} I\{Aut(S_0) \to Aut(S_i)\}_I.
  2. Given a family {S i} I\{S_i\}_I of inhabited equinumerous sets, there exists a family (x i) I(x_i)_I such that x i∈S ix_i \in S_i for all i∈Ii \in I.

Uniqueness of Constructions

It is well-known that objects defined by universal properties in a category, such as limits and colimits, are not unique on the nose, but only unique up to unique canonical isomorphism. It can be tempting to suppose that in a skeletal category, where any two isomorphic objects are equal, such objects will in fact be unique on the nose. However, under the most appropriate definition of β€œunique,” this is not true (in general), because of the presence of automorphisms.

More explicitly, consider the notion of cartesian product in a category. Although we colloquially speak of β€œa product” of objects AA and BB as being the object AΓ—BA\times B, strictly speaking a product consists of the object AΓ—BA\times B together with the projections AΓ—Bβ†’AA\times B\to A and AΓ—Bβ†’BA\times B\to B which exhibit its universal property. Thus, even if the category in question is skeletal, so that there can be only one object AΓ—BA\times B that is a product of AA and BB, in general this object can still β€œbe the product of AA and BB” in many different ways.

For example, given any projections AΓ—Bβ†’AA\times B\to A and AΓ—Bβ†’BA\times B\to B that exhibit AΓ—BA\times B as a product of AA and BB, we can compose them both with any automorphism of AΓ—BA\times B to get a new, different, pair of projections that also exhibit AΓ—BA\times B as a product of AA and BB. In fact, the universal property of a product implies that any two pairs of projections are related by an automorphism of AΓ—BA\times B, so this example is generic. Thus, even in a skeletal category, we cannot speak of β€œthe” product of AA and BB, except in the same generalized sense that makes sense in any category. A formal way to say this is that the β€œcategory of products of AA and BB,” while still equivalent to the trivial category, as it is in any category with products, will not be isomorphic to the trivial category even when the ambient category is skeletal.

(It is true in a few cases, though, that skeletality implies uniqueness on the nose. For instance, a terminal object can have no nonidentity automorphisms, so in a skeletal category, a terminal object (if one exists) really is unique on the nose.)

In intensional/homotopy type theory

All the discussion above pertains to set-level foundations. In intensional type theory such as homotopy type theory, additional care is needed.

A first guess is to define a precategory CC to be skeletal if for any objects a,ba,b there is a function β€–aβ‰…bβ€–β†’(a=b)\Vert a\cong b\Vert \to (a=b), i.e. if aa and bb are merely isomorphic then they are equal. (Here β€–βˆ’β€–\Vert-\Vert denotes the propositional truncation.) However, if the type ob(C)ob(C) of objects is not a set, then a=ba=b is not a proposition, and so under this definition a category could β€œbe skeletal” in more than one way.

Arguably a better definition is to say that a precategory CC is skeletal if for any objects a,ba,b the canonical function

(a=b)→‖a≅b‖ (a=b) \to \Vert a\cong b\Vert

is an equivalence. Since ‖a≅b‖\Vert a\cong b\Vert is always a proposition, this entails that a=ba=b is also a proposition. Thus, this implies that ob(C)ob(C) is a set, i.e. that CC is a strict category.

Note the analogy between this condition and the notion of univalent category: the only difference is the propositional truncation. It follows that if a precategory is both skeletal and univalent, then a≅ba\cong b is always a proposition (since it is equivalent to its propositional truncation), and thus the category is gaunt. Indeed, the gaunt categories are precisely those that are both skeletal and univalent.

Unlike in set-level foundations, in intensional type theory not every precategory (and not even every univalent category) has a skeleton. Indeed, if the axiom sets cover fails, then there can be univalent categories that are not weakly equivalent to any strict category. For this reason, the notion of skeleton tends to be less useful outside of set-level foundations, although particular concrete examples may turn out to be skeletal.


All of the above examples are in fact gaunt: not only are any two isomorphic objects equal, but any isomorphism is an identity morphism.

  • The delooping of a group is a skeletal category that is not gaunt (unless the group is trivial). In intensional type theory, this is a non-univalent precategory; its Rezk completion is no longer skeletal according to the above improved definition.

Posets as skeleta of prosets

In terms of (n,r)-category-theory one may essentially identify preordered sets with thin categories or (0,1)-categories. Under this identification, the passage of skeleta of categories corresponds to choosing an equivalent partial order inside a preorder.

For more details (and more precise statements, see at relation between preorders and (0,1)-categories.


See also:

Presenting a pretorsion theory on Cat whose torsion(-free) objects are the groupoids (skeletal categories, respectively), hence whose β€œtrivial objects” are the skeletal groupoids:

Last revised on February 1, 2024 at 12:25:49. See the history of this page for a list of all contributions to it.