arXiv · 2308.09371
The constructive content of a local-global principle with an application to the structure of a finitely generated projective module
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.
Explore related subjects
Keep this discovery
Henri Lombardi. 2023-08-18. The constructive content of a local-global principle with an application to the structure of a finitely generated projective module. https://arxiv.org/abs/2308.09371
Cite the original work for its findings. Save a collection to share your selection of sources.