Zulip Chat Archive

Stream: maths

Topic: ordered rings


view this post on Zulip Greg Price (Apr 06 2021 at 05:53):

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. R[ϵ]/(ϵ2) \mathbb{R}[\epsilon] / (\epsilon^2) with the lexicographic order where 0<sϵ<r 0 < s \epsilon < r for any reals r,s>0 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 R[ϵ]/(ϵ2) \mathbb{R}[\epsilon] / (\epsilon^2) an ordered ring, but I don't know if that's standard.

view this post on Zulip Greg Price (Apr 06 2021 at 06:01):

Also the docstring doesn't mention the 01 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 xy x \leq y only if x=y x = y , would qualify.

Conversely if 10 1 \leq 0 then 01 0 \leq -1 by subtraction and so 01 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.

view this post on Zulip Greg Price (Apr 06 2021 at 06:04):

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?

view this post on Zulip Greg Price (Apr 06 2021 at 06:07):

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)


Last updated: May 09 2021 at 09:11 UTC