The constructive content of a local-global principle with an application to the structure of a finitely generated projective module

TL;DR

This paper provides a constructive approach to understanding the structure of idempotent matrices over rings, revealing their local-global properties and advancing the Hilbert programme in algebra.

Contribution

It explicitly constructs orthogonal idempotents and localizations of matrices over rings, offering a constructive proof of local-global principles in algebra.

Findings

Explicit orthogonal idempotents for matrices over rings

Finite comaximal elements revealing local freeness

Constructive interpretation of local-global principles

Abstract

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.