Is every commutative ring having the invariant basis number property equivalent to AC? The proof I know that every commutative ring has the invariant basis number property involves quotienting by a maximum ideal to get a field, and so reducing to the case where the commutative ring is a field, for which the result is already proven. I wondered if there might be a "direct" proof, and tried to formalize it like this.
The fact that every commutative ring has a maximal ideal is proven with Zorn's lemma, and I suspect is in fact equivalent to Zorn's lemma. If we work in a set theory without Zorn's lemma/AC, is it still true that every commutative ring has the invariant basis number?
 A: It's not equivalent to the axiom of choice, although it may well need some weak form of choice.
It is well-known that the statement that every commutative ring has a prime ideal is strictly weaker than AC.
If $\mathfrak{p}$ is a prime ideal of $R$, and $K$ is the field of fractions of the integral domain $R/\mathfrak{p}$, then the rank of a free $R$-module $F$ is the $K$-dimension of $F\otimes_RK$.
A: We do not need axiom of choice to show that commutative rings have invariant basis number property. We can prove it with the help of exterior algebra $\wedge(V)$. Let $A$ be a commutative ring. First of all, it is obvious that if $m>n$, the $A$-module $\wedge^m(A^n)=0$ by considering a basis $p_1,p_2,...p_n$ and writing each element of $A^n$ in terms of the basis. Now we will show that $\wedge^n(A^n)$ is not $0$, by providing a surjective homomorphism onto $A$. Take a labelled basis $p_1,p_2,...p_n$ of $A^n$. Now for any permutation $\sigma$ in $S_n$ and elements $a_1,a_2,...a_n$ in $A$, send $a_1*p_{\sigma(1)} \wedge a_2*p_{\sigma(2)} .... \wedge a_n*p_{\sigma(n)}$ to $s(\sigma)*a_1a_2....a_n$ where $s(\sigma)$ is the sign of the permutation. Check that this uniquely extends to a surjective homomorphism $\wedge^n(A^n) \rightarrow A$ by bilinearity and the $v \wedge v=0$ property of the exterior algebra. Thus if $A$ is commutative and not trivial, $\wedge^n(A^n)$ isn't trivial. Now if $A^m$ and $A^n$ are isomorphic for some $m \neq n$, if we take $m>n$ WLOG, we see that there is a surjective homomorphism from $0=\wedge^m(A^n)=\wedge^m(A^m)$ to $A$, contradiction as $A$ is non-trivial. Thus non-trivial commutative rings satisfy IBN property.
A: The statement that nonzero commutative rings enjoy the invariant basis number property is true without any form of choice. In fact, it even holds in constructive mathematics, so without using the law of excluded middle.
A proof is contained in Fred Richman's three-page jewel Nontrivial uses of trivial rings. More specifically, he shows that:

Let $A$ be a commutative ring.

*

*If there is a linear injection $A^n \to A^m$ with $n > m$, then $1 = 0$ in $A$.

*If there is a linear surjection $A^n \to A^m$ with $n < m$, then $1 = 0$ in $A$.


The proof is fully explicit, showing how one can derive the equation $1 = 0$ from the (conditional) equations expressing the assumptions.
