Re: [Haskell-cafe] adjoint of coproduct & diagonal

On Sun, 2008-08-03 at 00:52 -0700, Jason Dusek wrote:

Derek Elkins wrote:

...

Jason Dusek wrote:

...

the unique arrow that goes from A+B to C+C is f+g -- but that would make C+C just the same as C.

The unique arrow is f* : (A,B) -> (C,C), -not- an arrow A+B -> C+C. An arrow f : A+B -> C does -not- uniquely determine an arrow A+B -> C+C such that the universal arrow diagram commutes.

Yes, I have confused my meaning a bit. +(f*) is also unique, and that was the arrow I was thinking of.

Again, f* is what is being solved for and proved unique.

So, we have f* : (A, B) -> (C, C), comprising h and k, so I am not sure sure how + will act on it. As I've seen with + so far, it works like this on arrows:

+((A -> C), (B -> C)) |-> A+B -> C

So, for example, +(f, g) |-> [f,g] -- so what is f* made of? This is what seems to be happening:

+((A, B) -> (C, C)) |-> A+B -> C+C

So how are h and k paired? Their pairing puts them CxC but seemingly in a different way from the way I've paired f and g.

The notation (A,B) is the notation for an object in a product category in this case. It is also the notation for a product in a category. Usually context makes it clear which is which. The notation f+g is the notation for the functorial action of + : CxC -> C on arrows, that is, if f : A -> B and g : C -> D then f+g : A+C -> B+D. One issue you seem to have is with the notation which is admittedly rather ambiguous. Another is with the precise definition of universal arrow. e : FY -> B is a universal arrow (from F) iff forall A and forall f : FA -> B there exists a unique arrow g : A -> Y such that e . Fg = f I prefer the representability perspective on universal arrows and that can be arrived at by essentially Skolemizing the above definition. If we have a function f : X -> Y then forall x in X there exists a y in Y namely f(x). Adding that y must be unique adds the requirement that f be injective. Taking this we can rewrite the above as e : FY -> B is a universal arrow (from F) iff there exists an injective function t : Hom(FA,B) -> Hom(A,Y) forall A such that forall f : FA -> B (that is forall f in Hom(FA,B)) e . F(t(f)) = f Since for any arrow g : A -> Y e . Fg = e . Fg and thus g = t(e . Fg) by uniqueness, we find that t is actually surjective as well as injective, that is -every- function A -> Y is in the image of t. A function is injective and surjective iff it is a isomorphism. So we can simplify the above. e : FY -> B is a universal arrow (from F) iff forall A there is an isomorphism Hom(FA,B) ~ Hom(A,Y) This can be further simplified by the definition of a natural isomorphism in Set. e : FY -> B is a universal arrow (from F) iff there is a natural isomorphism Hom(F-,B) ~ Hom(-,Y) The derivation of this definition captures the general pattern for all proofs of the statements along the line of your original question. There are three definitions of adjunction: one that uses representability (i.e. an isomorphism of homsets like the last definition of universal arrow above), one that uses universal arrows (i.e. assume either the unit or the counit is component-wise a universal arrow for all components), and one that uses the triangle identities. It is a crucial skill to be able to switch between these definitions seamlessly.