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 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⁻¹R 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 R_p. 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.