Rank of a free module without the axiom of choice Perhaps my question is really naive. I teach this semester in algebra. I am embarassed about the proof that a free module over an integral domain has a well-defined rank. It is based on the theorem that two bases have the same cardinal. But the proof I know of this statement uses a reduction modulo a maximal ideal (then we are brought back to the theory of vector spaces). It seems to me that the existence of a principal ideal needs in general the axiom of choice (not for concrete domains, of course). Whence my question:

Do we really need the axiom of choice to prove in full generality that the bases of a free module have the same cardinal ? 

One day later. I did not realize that the question even makes sense in the context of vector spaces. I'd like being able to accept a comment.
 A: Hans Läuchli [Auswahlaxiom in der Algebra, Comment. Math. Helv. 37, MR0143705, DOI:10.5169/seals-28602] has constructed a model of ZFA wherein a vector space has two bases of different size. (See also Jech, The Axiom of Choice, §10.3, problem 5.) The Jech–Sochor Embedding Theorem allows to transfer the result to ZF.
A: Let $A$ and $B$ be infinite sets. Let $M$ be a rank $|B|$ module
with basis $e_b$ for $b\in B$. If we take $|A|$ elements $m_a$ of $M$, then each can
be expressed in terms of finitely many of the $e_b$. If $B$ is not the union
of $|A|$ finite sets, then there is some $e_b$ not expressible in terms of the
$m_a$, so $M$ cannot be free on $|A|$ generators.
I'm not expert on set theory without AC, but those here who are will surely
tell us if there are models of ZF with non-equinumerous infinite sets
such that $A$ is the union of $|B|$ finite sets and vice versa.
A: If $F$ has a basis of size $n$, then it is not hard to show that there exist nonzero alternating $k$-linear maps $F^k\to R$ if and only if $k\leq n$.  Given this, it is clear that $F$ cannot have a basis of size different from $n$.  I think that is cleaner than any approach involving row-reduction or tensoring with a field.  To make it work in the presence of 2-torsion, you need to define 'alternating' in the right way: the function must vanish if any two arguments are equal, which is stronger than saying that the sign changes when any two arguments are swapped.
A: This is not so much an answer, as a (long) comment to Robin Chapman's answer. Robin writes

I'm not expert on set theory without AC, but those here who are will surely tell us if there are models of ZF with non-equinumerous infinite sets such that $A$ is the union of ${}|B|$ finite sets and vice versa.

I've thought about this question, and I have now convinced myself that there is an open problem here. 
(There may be a completely different way of approaching this, but) what looks to me to be the natural approach starts by rephrasing the question in the setting of the dual Schroeder-Bernstein theorem, since Robin's condition says that $A$ and $B$ are surjective images of each other, and each map is finite-to-one (at least if the finite sets are pairwise disjoint).
Since Benjamin Miller had worked on questions of this nature, I asked him about this version. He agreed that the expected example of such sets $A$ and $B$ would come from finding countable Borel equivalence relations $F_0 \subseteq F_1 \subseteq F_2$ on some Polish space $X$ of finite index over one another such that $X / F_0$ and $X / F_2$ are Borel isomorphic, but $X / F_0$ and $X / F_1$ are not universally measurably isomorphic.
Once we have this setting, it is standard how, for example, in models of the axiom of determinacy, we get that $A=X/F_0$ and $B=X/F_1$ are the sets we are looking for.
However, Ben mentioned that his guess was that doing this is a bit finer than what rigidity techniques (the main technical tool in these results) can handle currently. Ben asked around to a few experts, and they agreed with him in this regard.
A: You should tensor with the fraction field instead.
EDIT: I interpreted the question to mean "Given that I know that the dimension of a vector space is well-defined, how can I show that the rank of any free module over a domain is, avoiding Choice?".  I feel that this should be clarified since most of the other responses are addressing the more general question of how to avoid Choice altogether, though certainly my answer is not as informative.
