# Is an arbitrary product of sets a set?

$(A_{\alpha})_{\alpha\in B}$ a family of sets indexed by a set $B$. Is $\Pi _ {\alpha\in B} \ A_{\alpha}$ a set? I can see that it is a set if $A_{\alpha}=A \ \ \forall\alpha$ because in that case the product is a subset of the power set ${\cal P}\ (A\times B)$. As far as I understand, the axiom of choice only says the product is not the empty set, and it doesn't say if it is a set at all. Or am I wrong?

-
At least, this is true in a Grothendieck universe. –  Akhil Mathew Jul 18 '10 at 23:09
True; indeed, this is one of the axioms for a Grothendieck universe, but in SGA there is no definition of what a "family" of sets is. –  Thomas Scanlon Jul 19 '10 at 0:42

The standard definition of $(A_\alpha)_{\alpha \in B}$ a family of sets indexed by a set $B$ is that one is given a function $A$ with domain $B$ so that for $\alpha \in B$ we understand $A_\alpha$ as $A(\alpha)$. Then, yes, the product is a set.

The function $A$ itself is an element of the powerset of $B \times \text{ran}(A)$ (where $\text{ran}(A)$ is the range of $A$) and the product $\prod_{\alpha \in B} A_\alpha$ is by definition the set of functions $f$ with domain $B$ having the property that $(\forall \alpha \in B) f(\alpha) \in A(\alpha)$. As such, one proves that the product exists by applying the comprehension axiom to the above defining formula observing that any such $f$ will be an element of the powerset of $B \times \bigcup \text{ran} A$.

[And yes, the Axiom of Choice merely says that the product is nonempty if all of the $A_\alpha$ are nonempty.]

-
Thanks for your answer. The argument seems to go through even if $A_{\alpha}$ are not sets (but proper classes). So presumably a product of any objects is a set as long as it's indexed by a set? –  ashpool Jul 19 '10 at 1:12
No, if any of the $A_\alpha$s is a class, then the product is not a set. In the above argument, I used the fact that $A$ is a function, and in particular, is a set. –  Thomas Scanlon Jul 19 '10 at 1:29
What this does show, though, is that we can at least form a class representing the product of a family of classes, indexed by a set. There is no way (in any formal system I know) to form a product indexed by a proper class. –  Peter LeFanu Lumsdaine Jul 19 '10 at 11:01

Just to further clarify Thomas' correct answer, there is no such thing as a family of classes. A family of sets can be indexed by a proper class, and then is itself a proper class, but their is no family that has proper classes among its $A_\alpha$'s. Note however that a family of sets that is indexed by a class does not have a product since the elements of the this "product" would have to be proper classes. But only sets can be elements of something. Proper classes are not elements of anything. In fact, in ZFC (Zermelo-Fraenkel Set Theory plus Axiom of Choice) classes only exist in the form of formulas that define classes.

-
What you say is true, but nevertheless one can consider a family of classes, not by placing them as elements into another class, but by providing a uniform presentation of them as slices of a single class. For example, if $W$ is a class consisting of pairs $(x,y)$ for $x$ in a class $I$, then we may let $W_x=\{y|(x,y)\in W\}$, and regard $W$ as a uniform presentation of the classes $W_x$ for $x\in I$. The product here is a meta-class, consisting of class functions. One can prove individual such functions exist in GBC, but there will generally be no uniform presentation of all of them. –  Joel David Hamkins Jul 19 '10 at 10:50
Classes aren't elements of anything, but “a family of classes” does make sense. Formally[1], a proper class is a formula with a free variable, so the class “fields” is represented as “$x$ is a field”; a family of classes is a formula with two free variables, one thought of as a parameter; e.g. “$x$ is a field of characteristic $p$” is the family “fields of char $p$”, indexed over ℕ. As this example shows, we use them all the time without thinking about it! (More generally, a family of classes is given by the fibres of a class function.) [1] this goes for most standard systems, eg ZFC. –  Peter LeFanu Lumsdaine Jul 19 '10 at 13:06