Editing Coproduct (section)

== Discussion ==

The coproduct construction given above is actually a special case of a [[colimit]] in category theory. The coproduct in a category <math>C</math> can be defined as the colimit of any [[functor]] from a [[discrete category]] <math>J</math> into <math>C</math>. Not every family <math>\lbrace X_j\rbrace</math> will have a coproduct in general, but if it does, then the coproduct is unique in a strong sense: if <math>i_j:X_j\rightarrow X</math> and <math>k_j:X_j\rightarrow Y</math> are two coproducts of the family <math>\lbrace X_j\rbrace</math>, then (by the definition of coproducts) there exists a unique [[isomorphism]] <math>f:X\rightarrow Y</math> such that <math>f \circ i_j = k_j</math> for each <math>j \in J</math>.

As with any [[universal property]], the coproduct can be understood as a universal morphism. Let <math>\Delta : C\rightarrow C\times C</math> be the [[diagonal functor]] which assigns to each object <math>X</math> the [[ordered pair]] <math>\left(X, X\right)</math> and to each morphism <math>f : X\rightarrow Y</math> the pair <math>\left(f, f\right)</math>. Then the coproduct <math>X + Y</math> in <math>C</math> is given by a universal morphism to the functor <math>\Delta</math> from the object <math>\left(X, Y\right)</math> in <math>C\times C</math>.

The coproduct indexed by the [[empty set]] (that is, an ''empty coproduct'') is the same as an [[initial object]] in <math>C</math>.

If <math>J</math> is a set such that all coproducts for families indexed with <math>J</math> exist, then it is possible to choose the products in a compatible fashion so that the coproduct turns into a functor <math>C^J\rightarrow C</math>. The coproduct of the family <math>\lbrace X_j\rbrace</math> is then often denoted by 
: <math>\coprod_{j\in J} X_j</math>
and the maps <math>i_j</math> are known as the '''[[inclusion map|natural injections]]'''.

Letting <math>\operatorname{Hom}_C\left(U, V\right)</math> denote the set of all morphisms from <math>U</math> to <math>V</math> in <math>C</math> (that is, a [[hom-set]] in <math>C</math>), we have a [[natural isomorphism]] 
: <math>\operatorname{Hom}_C\left(\coprod_{j\in J}X_j,Y\right) \cong \prod_{j\in J}\operatorname{Hom}_C(X_j,Y)</math>
given by the [[bijection]] which maps every [[tuple]] of morphisms
: <math>(f_j)_{j\in J} \in \prod_{j \in J}\operatorname{Hom}(X_j,Y)</math>
(a product in '''Set''', the [[category of sets]], which is the [[Cartesian product]], so it is a tuple of morphisms) to the morphism
: <math>\coprod_{j\in J} f_j \in \operatorname{Hom}\left(\coprod_{j\in J}X_j,Y\right).</math>
That this map is a [[surjection]] follows from the commutativity of the diagram: any morphism <math>f</math> is the coproduct of the tuple 
: <math>(f\circ i_j)_{j \in J}.</math>
That it is an injection follows from the universal construction which stipulates the uniqueness of such maps.  The naturality of the isomorphism is also a consequence of the diagram.  Thus the contravariant [[hom-functor]] changes coproducts into products.  Stated another way, the hom-functor, viewed as a functor from the [[opposite category]] <math>C^\operatorname{op}</math> to '''Set''' is continuous; it preserves limits (a coproduct in <math>C</math> is a product in <math>C^\operatorname{op}</math>).

If <math>J</math> is a [[finite set]], say <math>J = \lbrace 1,\ldots,n\rbrace</math>, then the coproduct of objects <math>X_1,\ldots,X_n</math> is often denoted by <math>X_1\oplus\ldots\oplus X_n</math>. Suppose all finite coproducts exist in ''C'', coproduct functors have been chosen as above, and 0 denotes the [[initial object]] of ''C'' corresponding to the empty coproduct. We then have [[natural isomorphism]]s
: <math>X\oplus (Y \oplus Z)\cong (X\oplus Y)\oplus Z\cong X\oplus Y\oplus Z</math>
: <math>X\oplus 0 \cong 0\oplus X \cong X</math>
: <math>X\oplus Y \cong Y\oplus X.</math>
These properties are formally similar to those of a commutative [[monoid]]; a category with finite coproducts is an example of a symmetric [[monoidal category]].

If the category has a [[zero object]] <math>Z</math>, then we have a unique morphism <math>X\rightarrow Z</math> (since <math>Z</math> is [[terminal object|terminal]]) and thus a morphism <math>X\oplus Y\rightarrow Z\oplus Y</math>.  Since <math>Z</math> is also initial, we have a canonical isomorphism <math>Z\oplus Y\cong Y</math> as in the preceding paragraph.  We thus have morphisms <math>X\oplus Y\rightarrow X</math> and <math>X\oplus Y\rightarrow Y</math>, by which we infer a canonical morphism <math>X\oplus Y\rightarrow X\times Y</math>.  This may be extended by induction to a canonical morphism from any finite coproduct to the corresponding product.  This morphism need not in general be an isomorphism; in '''Grp''' it is a proper [[epimorphism]] while in '''Set'''<sub>*</sub> (the category of [[pointed set]]s) it is a proper [[monomorphism]].  In any [[preadditive category]], this morphism is an isomorphism and the corresponding object is known as the [[biproduct]].  A category with all finite biproducts is known as a [[additive category|semiadditive category]].

If all families of objects indexed by <math>J</math> have coproducts in <math>C</math>, then the coproduct comprises a functor <math>C^J\rightarrow C</math>.  Note that, like the product, this functor is ''covariant''.