Partially ordered ring
In abstract algebra, a partially ordered ring is a ring, together with a compatible partial order, i.e. a partial order on the underlying set A that is compatible with the ring operations in the sense that it satisfies:
and
for all. 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 where 's partially ordered additive group is Archimedean.
An ordered ring, also called a totally ordered ring, is a partially ordered ring where is additionally a total order.
An l-ring, or lattice-ordered ring, is a partially ordered ring where 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 is closed under addition and multiplication, i.e., if P is the set of non-negative elements of a partially ordered ring, then, and. Furthermore,.
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:
In any l-ring, the absolute value of an element x can be defined to be, where denotes the maximal element. For any x and y,
holds.
f-rings
An f-ring, or Pierce-Birkhoff ring, is a lattice-ordered ring in which and imply that for all. 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 be the space of all continuous, real-valued functions on X. is an Archimedean f-ring with 1 under the following point-wise operations:From an algebraic point of view the rings
are fairly rigid. For example, localisations, residue rings or limits of
rings of the form 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.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
, 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 is a commutative ordered ring, and. Then:
| by | |
| The additive group of A is an ordered group | OrdRing_ZF_1_L4 |
| iff | OrdRing_ZF_1_L7 |
| and imply and | OrdRing_ZF_1_L9 |
| ordring_one_is_nonneg | |
| OrdRing_ZF_2_L5 | |
| 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 is closed under multiplication iff A has no zero divisors. | OrdRing_ZF_3_L3 |
| If A is non-trivial, then it is infinite. | ord_ring_infinite |