Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
type: Item
instance of: scholarly article
title: Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
zbMATH Open document ID: 1493.68389
author: Thaynara Arielly de Lima
author: André Luiz Galdino
author: Andréia Borges Avelar
author: Mauricio Ayala-Rincón
published in: Journal of Automated Reasoning
publication date: 2022-01-21T00:00:00Z
review text: 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 onl…
reviewed by: Filippo Nuccio
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 13P99
Mathematics Subject Classification ID: 16Z05
Mathematics Subject Classification ID: 20N02
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7461270
zbMATH Keywords: PVS
zbMATH Keywords: ring theory
zbMATH Keywords: isomorphism theorems
zbMATH Keywords: principal ideals
zbMATH Keywords: prime ideals
zbMATH Keywords: maximal ideals
zbMATH Keywords: Chinese remainder theorem for rings
describes a project that uses: Isabelle
describes a project that uses: mathlib
describes a project that uses: PVS
MaRDI profile type: Publication
full work available at URL: s10817-021-09593-0
OpenAlex ID: W3163136021
Wikidata QID: Q113901238
cites work: Q3136877
cites work: Applied logic for computer scientists. Computational deduction and formal proofs
cites work: Exploring the structure of an algebra text with locales
cites work: Q4548814
cites work: Algèbre commutative
cites work: Q3497626
cites work: Formalized linear algebra over Elementary Divisor Rings in Coq
cites work: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
cites work: Formalizing ring theory in PVS
cites work: Q4379555
cites work: Noncommutative Rings and Their Applications
cites work: Euclidean self-dual codes over non-commutative Frobenius rings
cites work: Q4003421
cites work: A PVS Theory for Term Rewriting Systems
cites work: A constructive algebraic hierarchy in Coq.
cites work: A Machine-Checked Proof of the Odd Order Theorem
cites work: A Modular Formalisation of Finite Group Theory
cites work: Modelling algebraic structures and morphisms in ACL2
cites work: Q3105730
cites work: Q3884021
cites work: The first isomorphism theorem and other properties of rings
cites work: Q4301239
cites work: A Brief Overview of PVS
cites work: Q4264706
DOI: 10.1007/S10817-021-09593-0
description: scientific article; zbMATH DE number 7461270