constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In the same vein that commutative rings are to integral domains and GCD rings are to GCD domains, rings of fractions are to field of fractions.
Let be a commutative ring. A multiplicative submonoid of is a subset with an injection , an element and a function , such that and for all elements and , . The localization of away from a multiplicative submonoid is the initial commutative ring with a commutative ring homomorphism and a function , such that for all , .
The ring of fractions is the localization of away from the multiplicative subset of regular elements . Its elements are fractions where and which are by the definition the equivalence classes of pairs and iff . The addition is given by the formula
and multiplication by
For , , , and , division is given by
The ring of fractions of the integers is the rational numbers .
The ring of fractions of a discrete integral domain is a discrete field.
The ring of fractions of a Heyting integral domain is a Heyting field.
The ring of fractions of a strict approximate integral domain is a local ring.
The ring of fractions of any commutative ring is a prefield ring.
Michael Francis Atiyah, Ian Grant MacDonald. Introduction to Commutative Algebra. Addison-Wesley, 1969. (pdf, pdf)
Frank Quinn, Proof Projects for Teachers (pdf)
Max Zeuner, Univalent Foundations of Constructive Algebraic Geometry (arXiv:2407.17362)
Last revised on October 24, 2024 at 19:44:26. See the history of this page for a list of all contributions to it.