ordered rings

Stream: maths

[Greg Price]

On ordered_ring, the docstring doesn't seem to agree with the actual definition:

/-- An `ordered_ring α` is a ring `α` with a partial order such that
multiplication with a positive number and addition are monotone. -/
@[protect_proj]
class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)

The docstring says multiplication by a positive number should be monotone, but the definition goes further and requires it to be strictly monotone.

So for example the reals with first-order infinitesimals, i.e. $\mathbb{R}[\epsilon] / (\epsilon^2)$ with the lexicographic order where $0 < s \epsilon < r$ for any reals $r, s > 0$, are an ordered ring by the text definition but not the code definition, because $\epsilon$ is a zero divisor and so multiplication by $\epsilon$ is only non-strictly monotone.

Which definition is preferable? It seems natural to me to call something like $\mathbb{R}[\epsilon] / (\epsilon^2)$ an ordered ring, but I don't know if that's standard.

[Greg Price]

Also the docstring doesn't mention the $0 \leq 1$ condition. But I think that may only rule out pathological cases, and the fix is probably just to mention it in the docstring.

E.g. without that condition any ring with the discrete order, where $x \leq y$ only if $x = y$, would qualify.

Conversely if $1 \leq 0$ then $0 \leq -1$ by subtraction and so $0 \leq 1$ by multiplication, so either the ring is trivial or zero and one are incomparable. Though I can't quite pin it down to boring cases like the discrete order -- perhaps there are interesting examples.

[Greg Price]

I know ordered semirings are a messy area, from previous discussion:

Kevin Buzzard said:

The literature on ordered semirings is sparse and, in stark contrast to the usual conventions, no two definitions of an ordered semiring in the literature coincide. [… some details from a search of the literature …]

But for ordered rings perhaps a cleaner story is available?

[Greg Price]

Greg Price said:

The docstring says multiplication by a positive number should be monotone, but the definition goes further and requires it to be strictly monotone.

(On its face the axiom mul_pos is a bit narrower than this, but there's a lemma ordered_ring.mul_lt_mul_of_pos_left and its …_right counterpart, which show that the definition implies it is indeed strictly monotone)