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 is really an equivalence. For the weak inverse one forms a functor as follows. For every object one has chosen already the unique object in isomorphic to , but one also needs to make a choice of isomorphism for every . This enables to conjugate between and by
This correspondence makes a functor, that is the rule for morphisms is functorial. Let us show that is a weak inverse of . In one direction, for ; in another direction notice that for is an isomorphism. It suffices to show that these isomorphisms form a natural isomorphism ; 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