nLab
distributive category

Context

Monoidal categories

Category theory

Contents

Definition

Definition

A category CC with finite products ()×()(-)\times(-) and coproducts ()+()(-) + (-) is called (finitary) distributive if for any X,Y,ZCX,Y,Z\in C the canonical distributivity morphism

X×Y+X×ZX×(Y+Z) X\times Y + X\times Z \longrightarrow X\times (Y+Z)

is an isomorphism. The canonical morphism is the unique morphism such that X×YX×(Y+Z)X\times Y \to X\times (Y+Z) is X×iX\times i, where i:YY+Zi\colon Y\to Y +Z is the coproduct injection, and dually for X×ZX×(Y+Z)X\times Z \to X\times (Y+Z).

Remark

This notion is part of a hierarchy of distributivity for monoidal structures, and generalizes to distributive monoidal categories and rig categories. A linearly distributive category is not distributive in this sense.

This axiom on binary coproducts easily implies the analogous nn-ary result for n>2n\gt 2. In fact it also implies the analogous 0-ary statement that the projection

X×00 X\times 0 \to 0

is an isomorphism for any XX (see Proposition 2 below). Moreover, for a category with finite products and coproducts to be distributive, it actually suffices for there to be any natural family of isomorphisms X×Y+X×ZX×(Y+Z)X\times Y + X\times Z \cong X\times (Y+Z), not necessarily the canonical ones; see the paper of Lack referenced below.

A category CC with finite products and all small coproducts is infinitary distributive if the statement applies to all small coproducts. One can also consider κ\kappa-distributivity for a cardinal number κ\kappa, meaning the statement applies to coproducts of cardinality <κ\lt\kappa.

Any extensive category is distributive, but the converse is not true.

Properties

Proposition

In a category with products and coproducts, if products distribute over binary coproducts, then coproduct coprojections are monic.

Proof

Let i B:BB+Ci_B: B \to B + C be a coproduct coprojection, 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 coprojection

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 coprojection 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:AA×B\langle 1_A, f\rangle = \langle 1_A, g\rangle: A \to A \times B since 1 A×i B1_A \times i_B is monic. It follows that f=gf = g, as was to be shown.

Proposition

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

Proof

Clearly hom(X×0,Y)\hom(X \times 0, Y) is inhabited by X×00YX \times 0 \to 0 \to Y for any object YY. On the other hand, since the two coprojections 00+00 \to 0 + 0 coincide, the same holds for the two coprojections X×0(X×0)+(X×0)X \times 0 \to (X \times 0) + (X \times 0), by applying the distributivity isomorphism X×(0+0)(X×0)+(X×0)X \times (0 + 0) \cong (X \times 0) + (X \times 0). This is enough to show that any two maps X×0YX \times 0 \to Y coincide.

Proposition

In a distributive category, the initial object is strict.

Proof

Given an arrow f:A0f: A \to 0, we have that π A:A×0A\pi_A: A \times 0 \to A is a retraction of 1,f:AA×0\langle 1, f \rangle: A \to A \times 0, so that AA is a retract of A×00A \times 0 \cong 0. But retracts of initial objects are initial.

References

Revised on June 12, 2015 12:52:33 by Todd Trimble (67.81.95.215)