On Sat, 2008-08-02 at 20:00 -0700, Jason Dusek wrote:

Derek Elkins wrote:

...

h : A -> C and k : B -> C [...snip...] h : A -> B k : C -> D

Are these the same h and k?

No. As it says in the line just before what you quoted these are -any- h and k. They do end up being instantiated to the above h and k albeit with specializations of the latter types.

On Sat, 2008-08-02 at 23:40 -0700, Jason Dusek wrote:

Derek Elkins wrote:

...

[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.

This f is what I have labelled [f,g] (or f+g) in the diagram I linked to, right?

Yes. [f,g] is the right notation. The statement of the universal arrow, however, uses -any- arrow A+B -> C so I thought it best not to expose any of its structure. Anyway, showing that it has such structure is what proving uniqueness of f* does.

In that case h and k are just f and g, respectively, and 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.

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.

So I guess the Wikipedia page has an error in it? http://en.wikipedia.org/wiki/Coproduct#Definition -- _jsn

What about the part that reads: The unique arrow f making this diagram commute is then correspondingly denoted f1 ∐ f2 or f1 ⊕ f2 or f1 + f2 or [f1, f2] This would seem to say that [f,g] and f+g are the same thing -- but if I've understood Derek Elkins' remarks, the latter is the functorial action on arrows while the former is just the mediating arrow. -- _jsn

Derek Elkins wrote:

Jason Dusek wrote:

...

What about the part that reads:

The unique arrow f making this diagram commute is then correspondingly denoted f1 ∐ f2 or f1 ⊕ f2 or f1 + f2 or [f1, f2]

This would seem to say that [f,g] and f+g are the same thing -- but if I've understood Derek Elkins' remarks, the latter is the functorial action on arrows while the former is just the mediating arrow.

In my experience the functorial action of a functor on arrows almost always has the same symbol as the action on objects. Furthermore, I don't think I've ever seen an example where the symbol used for the action on objects was used for something other than the action on arrows. I do think I have seen examples when a different symbol was used. If A+B is used then f+g should be the action on arrows.

Admittedly wikipedia does violate this. Perhaps it's using conventions from some branch that I'm not familiar with. Maybe it is just silly.

Indeed. Using f1 ∐ f2 or f1 + f2 for the mediating arrow is confusing, to say the least. -- _jsn