# Partially ordered ring

In abstract algebra, a partially ordered ring is a ring (A, +, ·), together with a compatible partial order, that is, a partial order $\,\leq \,$ on the underlying set A that is compatible with the ring operations in the sense that it satisfies: $x\leq y{\text{ implies }}x+z\leq y+z$ and $0\leq x{\text{ and }}0\leq y{\text{ imply that }}0\leq x\cdot y$ for all $x,y,z\in A$. 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 $(A,\leq )$ where $A$'s partially ordered additive group is Archimedean.
An ordered ring, also called a totally ordered ring, is a partially ordered ring $(A,\leq )$ where $\,\leq \,$ is additionally a total order.
An l-ring, or lattice-ordered ring, is a partially ordered ring $(A,\leq )$ where $\,\leq \,$ is additionally a lattice order.

## Properties

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 $x$ for which $0\leq x,$ also called the positive cone of the ring) is closed under addition and multiplication, that is, if $P$ is the set of non-negative elements of a partially ordered ring, then $P+P\subseteq P$ and $P\cdot P\subseteq P.$ Furthermore, $P\cap (-P)=\{0\}.$
The mapping of the compatible partial order on a ring $A$ to the set of its non-negative elements is one-to-one; 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.
If $S\subseteq A$ is a subset of a ring $A,$ and:
* $0\in S$
* $S\cap (-S)=\{0\}$
* $S+S\subseteq S$
* $S\cdot S\subseteq S$
then the relation $\,\leq \,$ where $x\leq y$ if and only if $y-x\in S$ defines a compatible partial order on $A$ (that is, $(A,\leq )$ is a partially ordered ring).
In any l-ring, the absolute value $|x|$ of an element $x$ can be defined to be $x\vee (-x),$ where $x\vee y$ denotes the maximal element. For any $x$ and $y,$ $|x\cdot y|\leq |x|\cdot |y|$ holds.

## f-rings

An f-ring, or Pierce–Birkhoff ring, is a lattice-ordered ring $(A,\leq )$ in which $x\wedge y=0$ and $0\leq z$ imply that $zx\wedge y=xz\wedge y=0$ for all $x,y,z\in A.$ 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. The additional hypothesis required of f-rings eliminates this possibility.

### Example

Let $X$ be a Hausdorff space, and ${\mathcal {C}}(X)$ be the space of all continuous, real-valued functions on $X.$ ${\mathcal {C}}(X)$ is an Archimedean f-ring with 1 under the following pointwise operations: $[f+g](x)=f(x)+g(x)$ $[fg](x)=f(x)\cdot g(x)$ $[f\wedge g](x)=f(x)\wedge g(x).$
From an algebraic point of view the rings ${\mathcal {C}}(X)$ are fairly rigid. For example, localisations, residue rings or limits of rings of the form ${\mathcal {C}}(X)$ are not of this form in general. 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.

### Properties

* A direct product of f-rings is an f-ring, an l-subring of an f-ring is an f-ring, and an l-homomorphic image of an f-ring is an f-ring.
* $|xy|=|x||y|$ in an f-ring.
* The category Arf consists of the Archimedean f-rings with 1 and the l-homomorphisms that preserve the identity.
* Every ordered ring is an f-ring, so every sub-direct union of ordered rings is also an f-ring. Assuming the axiom of choice, a theorem of Birkhoff shows the converse, and that an l-ring is an f-ring if and only if it is l-isomorphic to a sub-direct union of ordered rings. Some mathematicians take this to be the definition of an f-ring.

## Formally verified results for commutative ordered 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.
Suppose $(A,\leq )$ is a commutative ordered ring, and $x,y,z\in A.$ Then:
| | by |
| The additive group of $A$ is an ordered group | OrdRing_ZF_1_L4 |
| $x\leq y{\text{ if and only if }}x-y\leq 0$ | OrdRing_ZF_1_L7 |
| $x\leq y$ and $0\leq z$ imply $xz\leq yz$ and $zx\leq zy$ | OrdRing_ZF_1_L9 |
| $0\leq 1$ | ordring_one_is_nonneg |
| $|xy|=|x||y|$ | OrdRing_ZF_2_L5 |
| $|x+y|\leq |x|+|y|$ | ord_ring_triangle_ineq |
| $x$ is either in the positive set, equal to 0 or in minus the positive set. | OrdRing_ZF_3_L2 |
| The set of positive elements of $(A,\leq )$ is closed under multiplication if and only if $A$ has no zero divisors. | OrdRing_ZF_3_L3 |
| If $A$ is non-trivial ($0\neq 1$), then it is infinite. | ord_ring_infinite |