In abstract algebra, a partially ordered ring is a ring (A, +, ·), together with a compatible partial order, that is, a partial order
on the underlying set A that is compatible with the ring operations in the sense that it satisfies:
[1] Various extensions of this definition exist that constrain the ring, the partial order, or both.
For example, an Archimedean partially ordered ring is a partially ordered ring
's partially ordered additive group is Archimedean.
[2] An ordered ring, also called a totally ordered ring, is a partially ordered ring
is additionally a total order.
[1][2] An l-ring, or lattice-ordered ring, is a partially ordered ring
is additionally a lattice order.
The additive group of a partially ordered ring is always a partially ordered group.
The set of non-negative elements of a partially ordered ring (the set of elements
also called the positive cone of the ring) is closed under addition and multiplication, that is, if
is the set of non-negative elements of a partially ordered ring, then
The mapping of the compatible partial order on a ring
to the set of its non-negative elements is one-to-one;[1] that is, the compatible partial order uniquely determines the set of non-negative elements, and a set of elements uniquely determines the compatible partial order if one exists.
defines a compatible partial order on
is a partially ordered ring).
denotes the maximal element.
They were first introduced by Garrett Birkhoff and Richard S. Pierce in 1956, in a paper titled "Lattice-ordered rings", in an attempt to restrict the class of l-rings so as to eliminate a number of pathological examples.
For example, Birkhoff and Pierce demonstrated an l-ring with 1 in which 1 is not positive, even though it is a square.
[2] The additional hypothesis required of f-rings eliminates this possibility.
be a Hausdorff space, and
be the space of all continuous, real-valued functions on
is an Archimedean f-ring with 1 under the following pointwise operations:
[2] From an algebraic point of view the rings
For example, localisations, residue rings or limits of rings of the form
A much more flexible class of f-rings containing all rings of continuous functions and resembling many of the properties of these rings is the class of real closed rings.
IsarMathLib, a library for the Isabelle theorem prover, has formal verifications of a few fundamental results on commutative ordered rings.
The results are proved in the ring1 context.
is a commutative ordered ring, and