If products distribute over coproducts, then coproduct inclusions are monic.

Let $i_B: B \to B + C$ be a coproduct inclusion, and suppose given maps $f, g: A \to B$ such that $i_B f = i_B g$. We observe that the coproduct inclusion

$i: A \times B \to A \times B + A \times C$

is monic because it has a retraction $(1_{A \times B}, \phi): A \times B + A \times C \to A \times B$. (All we need here is the existence of a map $\phi: A \times C \to A \times B$, for example the composite $A \times C \stackrel{\pi_A}{\to} A \stackrel{\langle 1_A, f \rangle}{\to} A \times B$.)

The composite of the coproduct inclusion $i$ with the canonical isomorphism $A \times B + A \times C \cong A \times (B + C)$, namely $1_A \times i_B: A \times B \to A \times (B + C)$, is therefore also monic. Given that $\langle 1_A, i_B f \rangle = \langle 1_A, i_B g \rangle: A \to A \times (B + C)$, we conclude

$(1_A \times i_B)\langle 1_A, f \rangle = \langle 1_A, i_B f \rangle = \langle 1_A, i_B g \rangle = (1_A \times i_B)\langle 1, g \rangle,$

whence $\langle 1_A, f\rangle = \langle 1_A, g\rangle$ since $1_A \times i_B$ is monic. It follows that $f = g$, as was to be shown.

While we’re at it:

If products distribute over binary coproducts, then products distribute over nullary coproducts (i.e., the projection $X \times 0 \to 0$ is an isomorphism for all objects $X$).

Clearly for any $Y$ the hom-set $\hom(X \times 0, Y)$ is inhabited by $X \times 0 \to 0 \to Y$, and so we only need show that any two $f, g: X \times 0 \to Y$ are equal. By the proposition above, it suffices that any two $f, g: X \times 0 \to X + Y$ are equal.

The coproduct inclusion $X \hookrightarrow X \times 0 + X$ is an isomorphism $X \cong X \times 1 \cong X \times (0 + 1) \cong X \times 0 + X \times 1 \cong X \times 0 + X$, so that the projection

$\hom(X \times 0, A) \times \hom(X, A) \to \hom(X, A)$

is an isomorphism of sets for any object $A$. As soon as $\hom(X, A)$ is inhabited, this means $\hom(X \times 0, A)$ must be a singleton. In particular, $\hom(X \times 0, X + Y)$ is a singleton, which is just what we wanted.

(There’s an easier proof of this, now recorded at the nLab. But this is what I first came up with.)

Revised on June 12, 2015 at 12:46:23
by
Todd Trimble