<abstract xmlns="http://www.w3.org/1999/xhtml">This article formalized rings of fractions in the Mizar system [3], [4]. A construction of the ring of fractions from an integral domain, namely a quotient field was formalized in [7].This article generalizes a construction of fractions to a ring which is commutative and has zero divisor by means of a multiplicatively closed set, say <italic>S</italic>, by known manner. Constructed ring of fraction is denoted by <italic>S</italic>~<italic>R</italic> instead of <italic>S−</italic>1<italic>R</italic> appeared in [1], [6]. As an important example we formalize a ring of fractions by a particular multiplicatively closed set, namely <italic>R \</italic> p, where p is a prime ideal of <italic>R</italic>. The resulted local ring is denoted by <italic>R</italic>p. In our Mizar article it is coded by <italic>R</italic>~p as a synonym.This article contains also the formal proof of a universal property of a ring of fractions, the total-quotient ring, a proof of the equivalence between the total-quotient ring and the quotient field of an integral domain.</abstract>

This article formalized rings of fractions in the Mizar system [3], [4]. A construction of the ring of fractions from an integral domain, namely a quotient field was formalized in [7].This article generalizes a construction of fractions to a ring which is commutative and has zero divisor by means of a multiplicatively closed set, say S, by known manner. Constructed ring of fraction is denoted by S~R instead of S−1R appeared in [1], [6]. As an important example we formalize a ring of fractions by a particular multiplicatively closed set, namely R \ p, where p is a prime ideal of R. The resulted local ring is denoted by Rp. In our Mizar article it is coded by R~p as a synonym.This article contains also the formal proof of a universal property of a ring of fractions, the total-quotient ring, a proof of the equivalence between the total-quotient ring and the quotient field of an integral domain.

Rings of Fractions and Localization

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

{"article-title":"Rings of Fractions and Localization"}

This article formalized rings of fractions in the Mizar system [3], [4]. A construction of the ring of fractions from an integral domain, namely a quotient...

Rings of Fractions and Localization

Publicado en línea: 29 may 2020

Páginas: 79 - 87

Aceptado: 13 ene 2020

DOI: https://doi.org/10.2478/forma-2020-0006

Palabras clave
rings of fractions, localization, total-quotient ring, quotient field

© 2020 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

Rings of Fractions and Localization

Publicado en línea: 29 may 2020

Páginas: 79 - 87

Aceptado: 13 ene 2020

DOI: https://doi.org/10.2478/forma-2020-0006

Palabras claverings of fractions, localization, total-quotient ring, quotient field

© 2020 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

Palabras clave
rings of fractions, localization, total-quotient ring, quotient field