Zulip Chat Archive

Stream: maths

Topic: Definition of ordered rings


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

Damiano Testa (Jan 13 2021 at 15:32):

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

Damiano Testa (Jan 13 2021 at 15:33):

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

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

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

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

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

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

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

Mario Carneiro (Jan 13 2021 at 15:42):

Ah yeah that was what I was thinking of

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

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.

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

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

Mario Carneiro (Jan 13 2021 at 17:30):

oh but you have to assume 0 < 1

Johan Commelin (Jan 13 2021 at 17:38):

which also make sense, I guess

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.

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: Dec 20 2023 at 11:08 UTC