Definition of ordered rings

Stream: maths

[Christopher Hoskin]

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]

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

[Damiano Testa]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

Ah yeah that was what I was thinking of

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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]

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]

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]

oh but you have to assume 0 < 1

[Johan Commelin]

which also make sense, I guess

[Christopher Hoskin]

@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]

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.