Todd Trimble
distributivity implies monicity of coproduct inclusions


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


Let i B:BB+Ci_B: B \to B + C be a coproduct inclusion, and suppose given maps f,g:ABf, g: A \to B such that i Bf=i Bgi_B f = i_B g. We observe that the coproduct inclusion

i:A×BA×B+A×Ci: A \times B \to A \times B + A \times C

is monic because it has a retraction (1 A×B,ϕ):A×B+A×CA×B(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 ϕ:A×CA×B\phi: A \times C \to A \times B, for example the composite A×Cπ AA1 A,fA×BA \times C \stackrel{\pi_A}{\to} A \stackrel{\langle 1_A, f \rangle}{\to} A \times B.)

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

(1 A×i B)1 A,f=1 A,i Bf=1 A,i Bg=(1 A×i B)1,g,(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 1 A,f=1 A,g\langle 1_A, f\rangle = \langle 1_A, g\rangle since 1 A×i B1_A \times i_B is monic. It follows that f=gf = 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×00X \times 0 \to 0 is an isomorphism for all objects XX).


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

The coproduct inclusion XX×0+XX \hookrightarrow X \times 0 + X is an isomorphism XX×1X×(0+1)X×0+X×1X×0+XX \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×0,A)×hom(X,A)hom(X,A)\hom(X \times 0, A) \times \hom(X, A) \to \hom(X, A)

is an isomorphism of sets for any object AA. As soon as hom(X,A)\hom(X, A) is inhabited, this means hom(X×0,A)\hom(X \times 0, A) must be a singleton. In particular, hom(X×0,X+Y)\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