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)→C is really an equivalence. For the weak inverse one forms a functor −′:x↦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 ix:x→x′ for every x. This enables to conjugate between C(x,y) and C(x′,y′) by
(xf→y)↦(x′i−1x→xf→yiy→y′).This correspondence makes −′ a functor, that is the rule for morphisms f′:=iy∘f∘i−1x is functorial. Let us show that −′ is a weak inverse of in. In one direction, (iny)′=y for y∈sk(C); in another direction notice that i−1inx′:inx′≅x for x∈C is an isomorphism. It suffices to show that these isomorphisms form a natural isomorphism i−1in:in−′→idC; 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