Zulip Chat Archive

Stream: maths

Topic: Definition of ordered rings


view this post on Zulip Christopher Hoskin (Jan 13 2021 at 15:29):

There seems to me to be something unsatisfactory about the mathlib definition of a (partially) ordered ring [1]. Specifically, it seems to me that

(mul_pos     :  a b : α, 0 < a  0 < b  0 < a * b)

ought to be

(mul_pos     :  a b : α, 0  a  0  b  0  a * b)

This is the axiom used in other locations e.g. [2], [3], [4]. More importantly the space of continuous real-valued functions on the unit interval is not an ordered ring according to the mathlib definition. (Consider two bump functions with disjoint supports.) Should we not expect a useful definition of ordered ring to include continuous bounded functions on a locally compact Hausdorff space?

Is there a reason mul_pos is specified the way it is?

Thanks,

Christopher

[1] https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ordered_ring.lean#L490-L492
[2] https://en.wikipedia.org/wiki/Ordered_ring
[3] https://isabelle.in.tum.de/library/HOL/HOL/Rings.html
[4] https://www.google.co.uk/books/edition/Lecture_Notes_On_Algebraic_Structure_Of/6vq2CgAAQBAJ?hl=en&gbpv=1&dq=ordered+rings&pg=PA20&printsec=frontcover

view this post on Zulip Damiano Testa (Jan 13 2021 at 15:32):

Just from a naming point of view, wouldn't your suggestion be called mul_nonneg?

view this post on Zulip Damiano Testa (Jan 13 2021 at 15:33):

https://leanprover-community.github.io/mathlib_docs/algebra/ordered_ring.html#mul_nonneg

view this post on Zulip Mario Carneiro (Jan 13 2021 at 15:34):

I think we just put the strongest properties we could get away with; there is a whole zoo of less constrained algebraic objects and it would be a lot of navel gazing to explore all of them, so we're just adding them as they become required for applications

view this post on Zulip Mario Carneiro (Jan 13 2021 at 15:35):

For conventional rings like int (or totally ordered rings more generally) it's no problem to have a rule like mul_pos

view this post on Zulip Mario Carneiro (Jan 13 2021 at 15:36):

it's certainly a theorem you want to be true in "some generality", so we need a class to represent it and the theorems that derive from it anyway

view this post on Zulip Reid Barton (Jan 13 2021 at 15:38):

I think linearly ordered rings should probably have this mul_pos property, but not general ordered rings

view this post on Zulip Mario Carneiro (Jan 13 2021 at 15:38):

I recall us investigating this a while ago. In fact I suspect the definition did not have mul_pos in it two years ago

view this post on Zulip Reid Barton (Jan 13 2021 at 15:39):

There was some discussion about related topics back in October (#4296, #4363) but I'm not sure about this specifically

view this post on Zulip Mario Carneiro (Jan 13 2021 at 15:42):

Ah yeah that was what I was thinking of

view this post on Zulip Mario Carneiro (Jan 13 2021 at 15:42):

from what I can tell this rule dates back at least to when ordered_ring was in core

view this post on Zulip Bryan Gin-ge Chen (Jan 13 2021 at 16:21):

The fact that mathlib's definition doesn't agree with other standard sources and there's no mention of it in the doc string is a problem. We could of course just add a doc string with a possible TODO for a bigger refactor.

view this post on Zulip Eric Wieser (Jan 13 2021 at 16:47):

Just as an exercises, these two definitions are equivalent if [no_zero_divisors R] is around:

example {R : Type*} [ring R] [partial_order R] :
  ( a b : R, 0 < a  0 < b  0 < a * b)  ( a b : R, 0  a  0  b  0  a * b) :=
begin
  intros h a b ha hb,
  by_cases haz : a = 0,
  { rw [haz, zero_mul], },
  by_cases hbz : b = 0,
  { rw [hbz, mul_zero], },
  have ha' := or.resolve_right (le_iff_lt_or_eq.mp ha) (ne.symm haz),
  have hb' := or.resolve_right (le_iff_lt_or_eq.mp hb) (ne.symm hbz),
  exact le_of_lt (h _ _ ha' hb'),
end

-- needed for the reverse direction
example {R : Type*} [ring R] [partial_order R] [no_zero_divisors R]:
  ( a b : R, 0  a  0  b  0  a * b)  ( a b : R, 0 < a  0 < b  0 < a * b) :=
begin
  intros h a b ha hb,
  cases le_iff_lt_or_eq.mp (h _ _ (le_of_lt ha) (le_of_lt hb)) with h1 h2,
  { exact h1, },
  exfalso,
  exact (eq_zero_or_eq_zero_of_mul_eq_zero h2.symm).rec (ne_of_gt ha) (ne_of_gt hb),
end

view this post on Zulip Mario Carneiro (Jan 13 2021 at 17:29):

In the isabelle version, it looks like mul_pos is derived from mul_nonneg over a total order. If that works that seems fine to me

view this post on Zulip Mario Carneiro (Jan 13 2021 at 17:30):

oh but you have to assume 0 < 1

view this post on Zulip Johan Commelin (Jan 13 2021 at 17:38):

which also make sense, I guess

view this post on Zulip Christopher Hoskin (Jan 13 2021 at 18:00):

@Damiano Testa From an Operator Algebra point of view, I'd use the term "positive" for "0 ≤ " and "strictly positive" for "0<". But that might not match Mathlib's conventions.

view this post on Zulip Floris van Doorn (Jan 13 2021 at 18:36):

Currently the only instance of ordered_ring in mathlib that is not linearly ordered is docs#filter.germ.ordered_ring. I think it would be good to change our definition to the standard definition.


Last updated: May 10 2021 at 07:15 UTC