[Haskell-cafe] adjoint of coproduct & diagonal

[Derek Elkins]

On Sun, 2008-08-03 at 00:52 -0700, Jason Dusek wrote:
> Derek Elkins <derek.a.elkins at gmail.com> 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.