Finite torsion-free abelian freeness by explicit rational coordinates without choice

On pairs $(a,n)$ with $a\in A$ and positive integer $n$, put $(a,n)\sim (b,m)$ when $ma=nb$. This is an equivalence relation. Reflexivity and symmetry are immediate. If $ma=nb$ and $pb=mc$, then $m(pa-nc)=0$, so torsion-freeness gives $pa=nc$, proving transitivity. Denote the class of $(a,n)$ by $[a,n]$ and its quotient set by $V$. Define $[a,n]+[b,m]=[ma+nb,nm]$, $-[a,n]=[-a,n]$, $0=[0,1]$, and $(r\mathrm{/}s)[a,n]=[ra,sn]$ for integer $r$ and positive integer $s$. These are independent of representatives: if $n^{\mathrm{\prime }}a=n{a}^{\mathrm{\prime }}$ and $m^{\mathrm{\prime }}b=m{b}^{\mathrm{\prime }}$, multiplying the first relation by $m{m}^{\mathrm{\prime }}$ and the second by $n{n}^{\mathrm{\prime }}$ gives the cross-multiplied equality for the two proposed sums. If also $r\mathrm{/}s=r^{\mathrm{\prime }}\mathrm{/}{s}^{\mathrm{\prime }}$, then $r{s}^{\mathrm{\prime }}=r^{\mathrm{\prime }}s$ and $s^{\mathrm{\prime }}{n}^{\mathrm{\prime }}ra=sn{r}^{\mathrm{\prime }}{a}^{\mathrm{\prime }}$, which gives the scalar equality. Negation and zero respect the relation as well.

For completeness, every subgroup $H\le {\mathbb{Z}}^d$ is free on at most $d$ elements, by induction on the finite integer $d$. The case $d=0$ has the empty basis. For $d>0$, project to the first coordinate. Its image is $c\mathbb{Z}$ by [F2]. The kernel is identified by the remaining coordinates with a subgroup of ${\mathbb{Z}}^{d-1}$, so the induction hypothesis gives it a basis of at most $d-1$ elements. If $c=0$, this kernel is all of $H$. If $c>0$, take one element $h\in H$ with first coordinate $c$. Every $x\in H$ has first coordinate $nc$ for a unique integer $n$, and $x-nh$ is in the kernel. Hence the kernel basis together with $h$ generates $H$. It is independent, because the first coordinate of a relation first forces the coefficient of $h$ to be zero, and then independence of the kernel basis forces all remaining coefficients to be zero. This proves the induction step for every subgroup, without assuming it is finitely generated in advance.

The operations make $V$ a rational vector space. Addition is commutative because $ma+nb=nb+ma$, and both associations of a three-term sum have representative $[mpa+npb+nmc,nmp]$ for inputs $[a,n],[b,m],[c,p]$. Zero is an identity and the negative sums to $[0,n^2]=[0,1]$. The identities $(r\mathrm{/}s)([a,n]+[b,m])=(r\mathrm{/}s)[a,n]+(r\mathrm{/}s)[b,m]$ and $(r\mathrm{/}s+t\mathrm{/}u)[a,n]=(r\mathrm{/}s)[a,n]+(t\mathrm{/}u)[a,n]$ follow by cross multiplication, reducing respectively to $r(ma+nb)=mra+nrb$ and $(ru+ts)a=rua+tsa$. Scalar associativity follows from $[rta,sun]$ for $(r\mathrm{/}s)(t\mathrm{/}u)[a,n]$, and scalar $1$ acts as the identity. These are all axioms in [F1]. The map $\eta :A\to V$, $\eta (a)=[a,1]$, is additive and injective, since $[a,1]=[0,1]$ forces $a=0$. Every $[a,n]$ equals $(1\mathrm{/}n)\eta (a)$, so $V$ is spanned over $\mathbb{Q}$ by the fixed finite list $\eta (a_1),\dots ,\eta (a_m)$.

Process that finite spanning list in its given order, retaining a vector exactly when it does not belong to the span of those previously retained. The resulting list $b_1,\dots ,b_r$ spans $V$, because each discarded vector was already in the span of an earlier retained sublist. It is independent: in a nonzero finite relation, the last vector with nonzero coefficient would belong to the span of the earlier ones, contrary to its retention rule. Thus it is a basis, constructed by a finite recursion rather than by an arbitrary basis-selection theorem. Each $\eta (a_j)$ has unique rational coordinates in this basis. Take $D>0$ to be the product of the positive denominators of the finitely many coordinates, using $D=1$ for the empty product. For $a\in A$, define $\mathrm{\Phi }(a)$ as $D$ times the coordinate vector of $\eta (a)$. Every $a$ is an integer linear combination of the $a_j$, so $\mathrm{\Phi }(a)\in {\mathbb{Z}}^r$. The map $\mathrm{\Phi }:A\to {\mathbb{Z}}^r$ is additive and injective, since $D\mathrm{\ne }0$, coordinates are unique and $\eta$ is injective.

Apply step 1.2 to $H=\mathrm{\Phi }(A)\le {\mathbb{Z}}^r$. Its finite basis and the injective map in step 3.1 identify $A$ with ${\mathbb{Z}}^t$ for some $t\le r$, giving the asserted finite freeness (rename $t$ to $r$ in the first assertion). The only selections were a single finite generating list, finitely many unique coordinate tuples, and at most one lift at each of finitely many integer-coordinate induction stages. Existence of such finitely many witnesses does not require any choice axiom. The explicit rationalization and integer-subgroup proof used no general PID structure or factorization theorem.