Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added a bit to skeleton about skeletons of internal categories
Entry skeleton says: “If the axiom of choice holds, then every category has a skeleton: simply choose one object in each isomorphism class.”
When the construction is simple, the proof is a tiny bit more subtle, namely one has to show that the inclusion $in:sk(C)\to C$ is really an equivalence. For the weak inverse one forms a functor $-':x\mapsto x'$ as follows. For every object $x$ one has chosen already the unique object $x'$ in $sk(X)$ isomorphic to $x$, but one also needs to make a choice of isomorphism $i_x:x\to x'$ for every $x$. This enables to conjugate between $C(x,y)$ and $C(x',y')$ by
$(x\stackrel{f}\to y)\mapsto (x'\stackrel{i_x^{-1}}\to x\stackrel{f}\to y\stackrel{i_y}\to y').$This correspondence makes $-'$ a functor, that is the rule for morphisms $f' := i_y\circ f\circ i_{x}^{-1}$ is functorial. Let us show that $-'$ is a weak inverse of $in$. In one direction, $(in_{y})' = y$ for $y\in sk(C)$; in another direction notice that $i^{-1}_{in_{x'}}:in_{x'}\cong x$ for $x\in C$ is an isomorphism. It suffices to show that these isomorphisms form a natural isomorphism $i^{-1}_{in}:in_{-'}\to id_C$; the naturality diagram is commutative precisely because of the conjugation formula for the functor $-'$ for morphisms.
Right ?
Right, it should say “simply choose one object in each isomorphism class and one isomorphism to that object from each other object in that class” (or something like that).
OK, I did.
1 to 6 of 6