i want to prove the following statement: Given a bicartesian closed category $\Bbb{A}$ (thus we have exponentials, finite products and finite coproducts) then the functor $F:\Bbb{A}\rightarrow\Bbb{A}$ given by $F(A)=A\times C$ for $C$ a fixed object in $\Bbb{A}$, thus $F(f)=f\times id$ for $f$ a morphism from $A$ to $B$, preserves the initial object and the binary coproduct (thus finite coproducts).
I have think over this and i make the following observations: We have to prove:
- $F(0)\cong 0\times C$
- $F(A+B)\cong F(A)+F(B)$ or equivalent $(A+B)\times C\cong A\times C+B\times C$
One morphism namely $f:(A+B)\times C\rightarrow A\times C+B\times C$ i can give by using the UMP's of product and coproduct. But what's about the other side? Do we have to use that $\Bbb{A}$ has exponentials (because otherwise this assumption is not nessesarry). Whats about the composition how to prove that we have the identity by composition?
Thank you for help.
On the contrary, it's an arrow $A \times C + B \times C \to (A + B) \times C$ which is canonically defined on the basis of universal mapping properties. Namely, if $i_A: A \to A + B$ and $i_B: B \to A + B$ denote the coproduct inclusions, then the pair
$$i_A \times 1_C: A \times C \to (A+B) \times C, \qquad i_B \times 1_C: B \times C \to (A+B) \times C$$
corresponds to a unique a map $A \times C + B \times C \to (A + B) \times C$, using the universal property of coproducts. It's this map that we want to prove is an isomorphism. Similarly, by the UMP of the initial object, there's a unique map $0 \to 0 \times C$ that we wish to prove is an isomorphism.
However, by cartesian closure, we have that the functor $- \times C$ is left adjoint to the functor $(-)^C$. The statement that left adjoints preserve colimits and in particular binary coproducts and the initial object, is exactly the statement that the canonical maps given above are isomorphisms. If you want the inverses explicitly, that can be done. We have coproduct inclusions
$$i_{A \times C}: A \times C \to A \times C + B \times C, \qquad i_{B \times C}: B \times C \to A \times C + B \times C$$
and by the adjunction, these correspond to maps
$$A \to (A \times C + B \times C)^C, \qquad B \to (A \times C + B \times C)^C$$
which induces a map from the coproduct:
$$A + B \to (A \times C + B \times C)^C$$
which again by the adjunction, corresponds to a map
$$(A + B) \times C \to A \times C + B \times C.$$
This is the desired inverse. The inverse of the map $0 \to 0 \times C$ is just the product projection $0 \times C \to 0$.
Edit: To be even more formulaic, let $e_X: X^C \times C \to X$ denote the evaluation map. This map is universal with respect to maps of the form $f: Y \times C \to X$, in the sense that to each such $f$ there is a unique map $\hat{f}: Y \to X^C$, called the currying of $f$, such that
$$f = (Y \times C \stackrel{\hat{f} \times 1_C}{\to} X^C \times C \stackrel{e_X}{\to} X).$$
(Taking in particular $1_{Y \times C}: Y \times C \to Y \times C$, its currying is a map $c_Y: Y \to (Y \times C)^C$ called the coevaluation at $Y$. This is just for general information; we don't have to use it.)
If $i_{A \times C}: A \times C \to A \times C + B \times C$ and $i_{B \times C}: B \times C \to A \times C + B \times C$ are the coproduct injections, and if for given maps $f: A \to X, g: B \to X$ we let $(f, g): A + B \to X$ denote the corresponding map out of the coproduct, then the inverse constructed above is
$$e_{A \times C + B \times C} \circ [(\widehat{i_{A \times C}}, \widehat{i_{B \times C}}) \times 1_C]: (A + B) \times C \to (A \times C + B \times C)^C \times C \to A \times C + B \times C.$$