Partially ordered ring

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 ≤ x , also called the positive cone of the ring) is closed under addition and multiplication, i.e., if P is the set of non-negative elements of a partially ordered ring, then P + P ⊆ P , and P ⋅ P ⊆ P . Furthermore, P ∩ ( − 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 is a subset of a ring A, and:

1. 0 ∈ S
2. S ∩ ( − S ) = { 0 }
3. S + S ⊆ S
4. S ⋅ S ⊆ S

then the relation ≤ where x ≤ y iff y − x ∈ S defines a compatible partial order on A (ie. ( A , ≤ ) is a partially ordered ring).

In any l-ring, the absolute value | x | of an element x can be defined to be x ∨ ( − x ) , where x ∨ y denotes the maximal element. For any x and y,

holds.

f-rings

An f-ring, or Pierce–Birkhoff ring, is a lattice-ordered ring ( A , ≤ ) in which x ∧ y = 0 and 0 ≤ z imply that z x ∧ y = x z ∧ y = 0 for all x , y , z ∈ 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 negative, even though being a square. The additional hypothesis required of f-rings eliminates this possibility.

Example

Let X be a Hausdorff space, and C ( X ) be the space of all continuous, real-valued functions on X. C ( X ) is an Archimedean f-ring with 1 under the following point-wise operations:

From an algebraic point of view the rings C ( X ) are fairly rigid. For example, localisations, residue rings or limits of rings of the form 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.

| x y | = | 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 subdirect 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 subdirect 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 , ≤ ) is a commutative ordered ring, and x , y , z ∈ A . Then: