## 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

#### 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

#### 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: May 10 2021 at 07:15 UTC