Making the use of maximal ideals constructive (Q2476020)

For a ring \(B\) and an integer \(n\geq 1\), denote by \(\text{E}_n(B)\) the subgroup of \(\text{SL}_n(B)\) generated by elementary matrices. For any ring \(A\), denote by \(\text{Res}(f,g)\) the resultant of two polynomials in \(A[X]\). A lemma of \textit{A. A. Suslin} [Math. USSR, Izv. 11, 221--238 (1977; Zbl 0378.13002)] states that, for a commutative ring \(A\), if \(\langle v_1(X),\dots,v_n(X)\rangle = A[X]\), where \(v_1\) is monic and \(n\geq 3\), then there exist \(\gamma_1,\dots,\gamma_l\in \text{E}_{n-1}(A[X])\) such that, denoting by \(w_i\) the first coordinate of \(\gamma_i \;{}^t(v_2,\dots,v_n)\), one has \(\langle \text{Res}(v_1,w_1),\dots, \text{Res}(v_1,w_l)\rangle=A\). Suslin's lemma played a central role in his second solution of Serre's problem on projective modules over polynomial rings. The present paper deciphers constructively the lemma, thus making possible Suslin's proof of Serre's problem to become fully constructive. Moreover, as the author writes in the abstract: ``the new method with which we treat this academic example may be a model for miming constructively abstract proofs in which one works modulo a generic maximal ideal in order to prove that an ideal contains \(1\)''.