[Haskell-cafe] adjoint of coproduct & diagonal
Derek Elkins
derek.a.elkins at gmail.com
Sat Aug 2 21:54:19 EDT 2008
On Sat, 2008-08-02 at 18:22 -0700, Jason Dusek wrote:
> I'm trying to figure out the adjunction diagrams for the
> adjunction where the diagonal functor is right adjoint to the
> coproduct functor. I'm |almost done|, but the co-unit has me
> stumped, because I can't figure out how the arrow at the top
> can be unique -- it seems it could be either one of:
>
> i_1 . [f,g]
> i_2 . [f,g]
>
> i_1, i_2 : C -> C+C
> f : A -> C
> g : B -> C
>
> The net effect of [id,id] on the right is to blur out the
> distinction. On #haskell, someone suggested there is a
> constraint I am missing; I've poked around for a day and still
> can't figure it out.
[id,id] is the counit.
[id,id] : C+C -> C
Given a function f : A+B -> C there exists a unique function
f* : (A,B) -> (C,C) that is a pair of functions
h : A -> C and k : B -> C such that
[id,id] . h+k = f.
The one way is obvious given f, h = f . inL and k = f . inR
So a solution exists.
To show that it is unique assume we are given an h and k such that the
above equation holds we need to show that h = f . inL (and similarly for
k.)
So start by precomposing both sides of the equation with inL giving:
[id,id] . h+k . inL = f . inL
We simply need to show that the left side is h. The injections together
form the unit. Naturality of the unit says that for any h and k:
h : A -> B
k : C -> D
inL . h = h+k . inL
inR . k = h+k . inR
Using this in the above we have:
[id,id] . inL . h = f . inL
Now we use one of the triangle identities which states:
[id,id] . inL = id
[id,id] . inR = id
and this finishes the proof:
id . h = f . inL
h = f . inL
More information about the Haskell-Cafe
mailing list