Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (Q2069874)

The paper under review reports about the formalization in the Prototype Verification System (PVS) of some fundamental results in ring theory. For the sake of this review, let us recall that, given a ring \(R\) and a ring homomorphism \(\varphi\colon R\to S\) to some other ring \(S\), the first isomorphism theorem guarantees the existence of an isomorphism \(\varphi\cong R/\ker\varphi\); the second theorem provides, for every ideal \(I\subset R\) and every subring \(H\subseteq R\), an isomorphism \(H/\bigl(H\cap I\bigr)\cong (H+I)/I\); and the third isomorphism theorem yields an isomorphism \(R/J\cong (R/I)/(J/I)\) for every ideal \(J\subseteq R\) containing \(I\). It should be clear from the very formulation of these three theorems that in order to formalize their statements -- and their proofs -- some ingredients are crucial: \begin{itemize} \item the notion of ring homomorphism; \item the notions of ideal and of subring; \item the notion of coset of a ring \(R\), or of an ideal \(J\), modulo a given ideal \(I\); \item the notion of quotient of a ring \(R\), or of an ideal \(J\), modulo an ideal \(I\). \end{itemize} Beyond formalizing these notions in PVS, the authors focus on some important properties of ideals (namely, what it means for an ideal to be \emph{principal}, or \emph{prime}, or \emph{maximal}); and they derive a crucial consequence of the first isomorphism theorem, normally known as the Chinese remainder theorem, stating that for pairwise comaximal ideals \(\{I_i\}_{1\leq i\leq n}\) in a commutative ring \(R\) there are isomorphisms. The comaximality assumption can be relaxed, as well as the commutativity assumption, yielding weaker yet interesting results: the formalization in this broader setting is presented in the paper, but we content ourselves with the stated version in this report. \[ R/(I_1\cap \cdots\cap I_n)\cong R/I_1\times\cdots \times R/I_n. \] Most of these theorems can already be found in some formalization systems, but in some cases only part of them are available. Concerning the PVS system itself, this paper marks an advance in that both the \texttt{ring} and the \texttt{algebra} theories only contained partial results and limited definitions, in particular concerning quotients, prior to the authors' work. The paper consists of nine sections, Section~1 being of introductory nature. In Section~2, all mathematical results are gathered, while the discussion of the formalization work itself is summarized in Sections~3--7; finally, Sections~8 and~9 contain descriptions of related and of future works. The text is clear and complete and it provides the reader with a clear and thorough description of the formalization work, emphasizing difficulties and relevant choices in detail. In most cases the authors have developed quite completely an API allowing to interact easily with the formalized notions, but three notable contributions do deserve special emphasis. Firstly, the authors chose to work in the setting of \emph{groupoids} (often rather called \emph{magmas} in the mathematical literature), simply consisting of sets endowed with one operation. The statements of the three isomorphism theorems can be extended to this setting, yielding more flexible and general results from which the special case of rings can be derived. Secondly, some stress is put on specific classes of ideals (namely, principal, prime and maximal ideals), having in mind their behaviour with respect to quotients: the (commutative) ring \(R/I\) is an integral domain if and only if \(I\) is a prime ideal, and \(R/I\) is a field if and only if \(I\) is maximal. Finally, it is noteworthy to observe that Section~7 is devoted to the explicit application of the Chinese remainder theorem for the ring \(\mathbb Z\), and the results described there might be of independent interest. It is clear that the authors were striving for a general set-up where the notions they consider could be further generalized, and this for the sake both of future applications and of the neatness of the formalization process. In this direction, generalizing quotients and isomorphism theorems to general groupoids, or magmas, is an important step, but the reviewer finds it a pity that the even more flexible notion of cosets with respect to an arbitrary equivalence relation was not implemented; it would allow not only to treat group and ring theory, but also quotients beyond the realm of algebraic structures (allowing, for example, to define quotient topological spaces or quotient metric spaces). In the same vein, developing a general theory for principal ideal domains might have preceded the special case \(R=\mathbb Z\); the authors indeed do address this point in Section~9.