Products and the axiom of choice

Question

Here: Universal property of the direct product, proof verification

Matematleta noted in the comments, that the definition of the product uses the axiom of choice by default. Why is that?

The definition i am looking at is simply:

For sets $X_1, X_2, \dotso, X_n$ is $\prod_{i= 1}^n X_i:=\{(x_1,\dotso, x_n)| x_1\in X_1,\dotso, x_n\in X_n\}$

Analogously for an arbitrary index set.

Also I always wondered, why you need the axiom of choice to state, that the product of not empty sets is not empty.

Answer 1

Because that's not a definition: what precisely is "$(x_1,...,x_n)$"? We might be tempted to hand-wave this away, and certainly nothing too surprising happens with finite tuples, but this is clearly unsatisfactory for arbitrary products - for example, what if I'm taking the product of a family of sets which isn't even linearly ordered in the first place?

• In general, never be satisfied when a definition you've written has all the "hard work" being done by the word "analogously" or something similar.

So we have to rigorously define what we mean by "large" ordered tuples.

Intuitively, an element of $\prod_{i\in I}X_i$ should be an "$I$-ary sequence" whose $i$th term comes from $X_i$. The simplest way to make this precise is to think of sequences as just being nicely-dressed functions - the sequence "First term $0$, second term $1$, third term $0$" is just the function with domain $\{1,2,3\}$ sending $1$ to $0$, $2$ to $1$, and $3$ to $0$.

Abstractly, then, we're talking about the following

An element of $\prod_{i\in I}X_i$ is a function $p:I\rightarrow\bigcup_{i\in I} X_i$ with $p(i)\in X_i$ for each $i\in I$.

Now to talk about functions it suffices to talk about ordered pairs, which we can do by e.g. Kuratowski's definition. So we've converted a single "ordered $I$-tuple" into a set of ordered pairs.

That explains where the definition comes from. And with this in mind it's clear that the nonemptiness of the product of nonempty sets is equivalent to the axiom of choice: a choice function for a family of disjoint nonempty sets is literally an element of the product of that family of sets!