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?
- 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.
Best Answer
So to answer my question, the proof is valid since:
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$).
As rschwieb remarked, since we only make finitely many choices there's no need of any strong choice principle.