For a given field $k$ and a set $X$ we want to define the ring $k[X]$ of polynomials with $X$ as the set of variables. We do not assume $X$ to be finite. And we want to do this without employing axiom of choice.
Informally, the elements of $k[X]$ will be finite sums of monomials of the form $cx_1^{k_1}\dots x_n^{k_n}$, where each monomial is determined by a coefficient $c\in k$, finitely many elements $x_1,\dots,x_n\in X$ and the exponents $k_1,\dots,k_n$, which are positive integers. Addition and multiplication of polynomials from $k[X]$ will be defined in the natural way. However, we also should be able to describe this algebraic structure more formally. Especially if we are trying to use it in some proof in the axiomatic system ZF. In this case it is also important to check that we have not used AC anywhere in the proof. (Using Axiom of Choice can easily be overlooked, especially if somebody is used to work in ZFC rather than ZF, i.e., without the restriction that AC should be avoided.)
To explain a bit better what I mean, this is similar to defining the polynomial ring $k[x]$ of polynomials in a single variable $x$. Informally, we view polynomials as expressions of the form $a_nx^n+\dots+a_1x+a_0$ (with $a_i\in k$). And we will also write them in this way. But formally they are sequences of elements of $K$ with finite support.
I will also provide below a suggestion how to construct $k[X]$ in ZF. I would be interested in any comments on my approach, but also if there are different ways to do this, I'd be glad to hear about them.
This cropped up in a discussion with some colleagues of mine.
Transfinite induction and direct limit
One colleague suggested the following approach, which clearly uses AC (in the form of the well-ordering theorem). But he said that this is the construction of $k[X]$ which seems the most natural to him.
- We take any well-ordering of the set $X=\{x_\beta; \beta<\alpha\}$.
- By a transfinite induction we define rings $k_\beta$ for $\beta\le\alpha$ and also an embeddings $k_\beta \hookrightarrow k_{\beta'}$ for any $\beta<\beta'<\alpha$. The ring $k_\beta$ is supposed to represent the polynomials using only variables $x_\gamma$ for $\gamma\le\beta$. We put $k_0=k[x_0]$. Similarly if $\beta$ is a successor ordinal we can define $k_\beta=k_{\beta-1}[x_\beta]$. If $\beta$ is a limit ordinal, then we can take $k_\beta$ as a direct limit of $k_\gamma$, $\gamma<\beta$.
- Then the ring $k_\alpha$ is $k[X]$ which we wanted to construct.
It is not immediately clear to me whether the proof can be simplified in the way that the direct limit can be replaced by union. However, I do not consider this to be an important difference, since using direct limit (especially in such a simple case, with linear order and embeddings) seem to me to be a rather standard approach for this type of constructions. And anybody with enough mathematical maturity to study a proofs of this level will probably not have a problem with the notion of direct limit.
The fact that this is indeed a ring (or even integral domain) follows from the fact that these properties are preserved by this simple version of direct limits. (I.e., direct limit based on linearly ordered system of rings with embeddings between them. This does not differ substantially from the proof that union of chain of rings is a ring.)
Functions with finite support
I have suggested this approach, which is more closely modeled after the case of ring in a single variable. Unless I missed something, this can be done in ZF, i.e., without use of ZFC.
Let us first try to definite the set $M$ of all monomials of the form $x_1^{k_1}\dots x_n^{k_n}$. (I.e., the monomials with the coefficient $1$.) Every such monomial is uniquely determined by a finite subset $F\subseteq X$ and a function $g: F\mapsto\mathbb N$, where $\mathbb N=\{1,2,\dots\}$. Or, if you will, $\mathbb N=\omega\setminus\{0\}$. (Since we are talking about finite sets, it might be worth mentioning that there are several notions of finite set in ZF. We take the standard one, which is sometimes called Tarski-finite or Kuratowski-limit. This notion of finiteness is well behaved. For our purposes it is important to know that union of finite set of finite sets is again finite and the same is true for Cartesian product.)
So we can get $M$ as a set of all pairs $(F,g)$ with the properties described above. Existence of such sets can be defined in ZF in a rather straightforward manner. (All properties of $F$ and $g$ can be described by a formula in a language of set theory. Clearly $F\in\mathcal P(X)$. Or we can use the set $\mathcal P^{<\omega}(X)$ of finite subsets of $X$ instead. The function $g$ belongs to the set of all functions from such $F$'s to $\mathbb N$. For each $F$ we have the set $\mathbb N^F$ consisting of all functions $F\to\mathbb N$. Then we can simply take the union $G=\bigcup\limits_{F\in\mathcal P(X)} \mathbb N^F$, based on axiom of union. The we use axiom scheme of specification to get only those pairs from $\mathcal P(X)\times G$ which have the required properties.)
Now we have the set $M$. We want to model somehow the finite sums of elements from $M$ multiplied by a coefficents from $k$. To this end we simply take the functions from $M$ to $k$ with finite support.
So far we have only defined the underlying set $k[X]$. We still need to define addition, multiplication, verify that this is integral domain. However, any polynomial $p\in k[X]$ only uses finitely many variables, since we have finitely many monomials and each of them only contains finitely many variables. If we are verifying closure under addition or multiplication, or some properties of integral domain such as associativity or distributivity, then any such condition only includes finitely many polynomials and thus we have only finitely many variables. So we can look at this condition as property of polynomials in $k[F]$, where $F$ is some finite subsets. Assuming we already know that polynomial ring in finitely many variables over a field $k$ is an integral domain, this argument can be used to argue that $k[X]$ is an integral domain, too.
The above discussion occurred in connection with the proof of Andreas Blass' result that existence of Hamel basis for vector space over arbitrary fields implies Axiom of Choice. This proof can be found for example in the references below. It is also briefly described in this answer.
In this proof the polynomials from $k[X]$ are used. (Then the field $k(X)$ of all rational functions in variables from $X$ is created – in the other words, the quotient field of $k[X]$. And the proof than uses existence of a Hamel basis of $k(X)$ considered as a vector space over a particular subfield of $k(X)$.)
Unless I missed something, the proofs given there do not discuss whether $k[X]$ can be constructed without AC. Which suggests that the authors considered this point to be simple enough to be filled in by a reader. So I assume that proof of this fact should not be too difficult. (Of course, if you know of another reference for a proof this results which also discusses this issue, I'd be glad to learn about it.)
- A. Blass: Existence of bases implies the axiom of choice. Contemporary Mathematics, 31:31–33, 1984. Available on the authors website
- Theorem 5.4 in L. Halbeisen: Combinatorial Set Theory, Springer, 2012. The book is freely available on the author's website.
- Theorem 4.44 in H. Herrlich Axiom of choice, Springer, 2006, (Lecture Notes in Mathematics 1876).
There are these related questions:
The answers given there can be considered somewhat similar to the approach I suggested above. However, it is not discussed there whether AC was used somewhere in this construction.
Best Answer
Your "functions with finite support" approach is the standard approach to take to this, and is very likely what any author who considers the question trivial has in mind. The correct notion of "finite" to take when defining monomials is the usual one, as you have done (this is necessary for the polynomial ring you get to be the free commutative $k$-algebra on its variables).
Just to give some evidence that this approach is standard, this is the definition of $k[X]$ used in Lang's Algebra, for instance. (Lang describes this construction rather tersely on page 106 as an example of the more general monoid algebra construction described on pages 104-5. Lang's construction of the set $M$ of monomials is a little different from yours: he defines it as a subset of the free abelian group on $X$, which he constructs as the group of finite-support functions $X\to\mathbb{Z}$ on page 38.)
Note that it is not actually necessary to observe that every polynomial involves only finitely many variables to define or verify the properties of addition and multiplication. Indeed, addition can just be defined pointwise on the coefficients and makes sense for arbitrary functions from $M$ to $k$. Multiplication also makes sense for arbitrary functions from $M$ to $k$ (which you can think of as formal power series): you just need to define the coefficient of a given monomial $x_1^{k_1}\dots x_n^{k_n}$ in a product, and you can do this by the usual convolution formula. You then just have to check that if two functions $M\to k$ each have finite support, then so does their product; this is straightforward (a monomial in the support of the product must be the product of monomials in the support of each of the factors). The verification of the basic properties of multiplication then works exactly as it does in the case of finitely many variables.