  We study the structure of an idempotent matrix $F$ over a commutative ring.
We make explicit the fundamental system of orthogonal idempotents, hidden in
this matrix, for each of which the matrix has a well-defined rank. Similarly we
find a finite number of comaximal elements of the ring which make explicit the
fact that the codomain of $F$ is locally free. Our proofs are based on the
abstract local-global principle. We give two methods to recover a constructive
proof of these results. The most interesting one is a constructive
interpretation of a very simple version of the abstract local-global principle.
We think we have made a significant step towards a constructive version of the
"Hilbert programme" for abstract algebra, i.e. the automatic translation of
proofs of abstract algebra into constructive proofs.
