How do we prove intuitionistically that free modules of finite rank are projective?

Question

I'm struggling to understand how the following proof can be intuitionistically valid$^1$:

Theorem. Let $R$ be a commutative ring. A free module of finite rank $R^n$ is projective.

Proof. Let $A \overset{g}\to B$ be an onto map of modules, let $R^n \overset{f}\to B$ be a map of modules. Let moreover $x_1, \ldots, x_n$ be a basis of $R^n$. Then there exist $a_1, \ldots, a_n \in A$ such that $g(a_i) = f(x_i)$ for $i=1,\ldots,n$. By universal property of the free modules then, the map $x_i \mapsto a_i$ can be extended to the desired map of modules $R^n \overset{h}\to A$.

This is the standard proof, and it is given in a constructive context e.g. in [MRR, p. 57].

However it seems to me that to choose elements $a_1, \ldots, a_n$ we must employ some kind of choice principle. Is this true?

---

1. This mean it doesn't lean on LEM (law of excluded middle, i.e. no arguing by contradiction), AC (axiom of choice), DC (axiom of dependent choice), AC$_\omega$ (axiom of countable choice).

---

[MRR] Mines, Richman, Ruitenburg; A course in constructive algebra, Springer-Verlag, 1988.

Answer 1

So to answer my question, the proof is valid since:

1. As Rob Arthan pointed out, we can extract the elements $a_1,\ldots,a_n$ from a proof of surjectivity of $g$ (which, intuitionistically, explicitly describes how to find at least one preimage for each element of $B$).

2. As rschwieb remarked, since we only make finitely many choices there's no need of any strong choice principle.

Answer 2

It might be helpful to reframe the theorem more generally.

Let $\mathcal{S}$ be a regular category, and let $\mathcal{T}$ be the category of models of a finitary algebraic theory. Let $F\dashv G:\mathcal{T}\to\mathcal{S}$ be the free-forgetful adjunction ($G$ preserves covers because $S$ is regular). Then $FS$ is projective in $\mathcal{T}$ whenever $S$ is projective in $\mathcal{S}$.

For given cover $g:A\to B$ and morphism $f:FS \to B$, consider the diagram with the adjunct $f' : S\to GB$ and $Gg : GA \to GB $. Then $Gg$ is a cover, so from $S$ being projective we get a map $h :S \to GA $ that "completes the triangle". Taking adjuncts again gets us $f=gh'$ for some $h' :FS \to A$.

---

Then the additional ingredient needed is that finite sets are projective. That's a theorem once you've chosen the correct notion of "finite set".