Patrick Stevens bio photo

Patrick Stevens

Former mathematics student at the University of Cambridge; now a software engineer.

Email Twitter Github Stackoverflow

Exercise 1 is easy: at the end of Chapter 2 the corresponding products statement was proved, and the obvious dual statement turns out to be this one.

Exercise 2 falls out of the appropriate diagram, whose upper triangle is irrelevant.

Free monoid functor preserves coproducts

Exercise 3 I’ve already proved - search on “sleep”.

Exercise 4: Let be given by , and likewise by . Claim: this has the UMP of the product of and . Indeed, if and are given, then is specified uniquely by (taking the disjoint union).

Exercise 5: Let the coproduct of be their disjunction. Then the “coproduct” property is saying “if we can prove from and from , then we can prove it from ”, which is clearly true. The uniqueness of proofs is sort of obvious, but I don’t see how to prove it - I’m not at all used to the syntax of natural deduction. I look at the answer, which makes everything clear, although I still don’t know if I could reproduce it. I understand its spirit, but not the mechanics of how to work in the category of proofs.

Exercise 6: we need that for any two monoid homomorphisms there is a monoid and a monoid homomorphism universal with . Certainly there is a monoid hom with that property (namely the trivial hom), so we just need to find one that is “big enough”. Let be the subset of on which , which is nonempty because they must be equal on . I claim that it is a monoid with ’s operation. Indeed, if and then . This also works with abelian groups - and apparently groups as well.

Finally we need that this structure satisfies the universal property. Let be a monoid with hom , such that . We want a hom with . But if then we must have the image of being in , so we can just take to be the inclusion. This reasoning works for abelian groups too. We relied on Mon having a terminal element and monoids being well-pointed.

Finite products: we just need to check binary products and the existence of an initial object. Initial objects are easy: the trivial monoid/group is initial. Binary products: the componentwise direct product satisfies the UMP for the product, since if then take by . This is obviously homomorphic, while the projections make sure it is unique.

Exercise 7 falls out of another diagram. The (1) label refers to arrows forced by the first step of the argument; the (2) label to the arrow forced by the (1) arrows.

Coproduct of projectives is projective

Exercise 8: an injective object is such that for any with arrows with monic, there is with . Let be posets, and let be monic. Then for any points we have , so is injective. Conversely, if is not monic then we can find with but . This means because the arrows agree on their domain; so we have and with . But , so we have not injective.

Now, a non-injective poset: we want to set up a situation where we force some extra structure on . If is has two distinct nontrivial chunks which have no elements comparable between the chunks, then is not injective. Indeed, let . Then the inclusion does not lift across the map which sends one chunk “on top of” the other: say one chunk is and the other , then the map would have image .

What about an injective poset? The dual of “posets” is “posets”, so we can just take the dual of any projective poset - for instance, any discrete poset. Anything well-ordered will also do, suggests my intuition, but I looked it up and apparently the injective posets are exactly the complete lattices. Therefore a wellordering will almost never do. I couldn’t see why failed to be injective, so I asked a question on Stack Exchange; midway through, I realised why.

Exercise 9: is obviously a homomorphism. Indeed, because is a homomorphism. But is the wordification of the letter , and likewise of , so we have is the word , which is itself the inclusion of the product .

Exercise 10: Functors preserve the structure of diagrams, so we just need to show that that the unique arrow guaranteed by the coequaliser UMP corresponds to a unique arrow in Sets. We need to show that given a function there is only one possible homomorphism which forgetful-functors down to it. But a homomorphism does specify where every single set element in goes, so uniqueness is indeed preserved.

Exercise 11: Let be the smallest equiv rel on with for all . Claim: the projection is a coequaliser of . Indeed, let be another set, with a function . Then there is a unique function with : namely, . This is well-defined because if then .

Exercise 12 I’ve already done - search on “wrestling”, though I didn’t write this up.

Exercise 13: I left this question to the end and couldn’t be bothered to decipher the notation.

Exercise 14: The equaliser of and is universal such that . Let and the inclusion. It is an equivalence relation manifestly: if and then , and so on.

The kernel of , the quotient by an equiv rel , is . This is obviously , since iff . That’s what it means to take the quotient.

The coequaliser of the two projections is the quotient of by the equiv rel generated by the pairs , as in exercise 11. This is precisely the specified quotient.

The final part of the exercise is a simple summary of the preceding parts.

Exercise 15 is more of a “check you follow this construction” than an actual exercise. I do follow it.