LinearOrderedRing

Stream: mathlib4

[Artie Khovanov]

The definition of a totally ordered ring (LinearOrderedRing) appears nonstandard to me -- it requires that multiplication be strictly monotonic, rather than merely monotonic; that is, it "additionally" requires the ring to be an integral domain. My "standard" definition is what is on Wikipedia, but apparently different textbooks give different definitions.

This came up when I was trying to refactor positive cones of rings to view them as special kinds of subsemiring. I think I will just force total positive cones to be defined over domains, since the nontrivial theory comes in for fields anyway.

Is there any particular reason why LinearOrderedRing is defined with this convention and not the other? And is there any need for the weaker version of the typeclass?

[Kevin Buzzard]

Do you know an example of a totally ordered ring which doesn't satisfy the axioms of docs#LinearOrderedRing ?

Seems that you can use docs#OrderedRing if you don't mind losing the fact that the order is total.

I just went through all the history of this by the way. This stuff was all in core initially (in Lean 3) and might well have been written by computer scientists with different applications in mind.

[Artie Khovanov]

Integers with trivial multipliciation and standard addition and order. Or if you want something more natural, R[eps]/eps^2 with eps infinitessimal (R can be any ordered ring really, but take the reals).

[Artie Khovanov]

It's not crucial for my application (I am working with fields, which are domains, and obviously the definitions are equivalent for domains), but I thought I would ask.

[Kevin Buzzard]

I don't know what "trivial multiplication" means on the integers (whilst preserving the axioms of a ring according to Lean) but I believe the infinitesimal example.

[Artie Khovanov]

oh yeah oops the integer example has no multiplicative unit

[Artie Khovanov]

I think there is more discussion at
https://math.stackexchange.com/questions/3822980/different-definitions-of-ordered-ring
Probably that is where I remember the examples from haha

[Scott Carnahan]

By the way, your "standard" definition agrees with Bourbaki Algebra ch. VI, which has the following exercise: Given a totally ordered commutative ring, show that the quotient by the ideal formed by the nilpotent elements is a totally ordered integral domain. Perhaps the mathlib version should be called StrictLinearOrderedRing instead.

[Artie Khovanov]

I know this would be a huge change but I kinda want to make it now I'm actually working on ordered ring theory that isn't just an abstraction of properties of the reals or whatever.

Something like
(move)LinearOrderedRing -> StrictLinearOrderedRing
(new) LinearOrderedRing extends OrderedRing, LinearOrder
(new) StrictLinearOrderedRing.toLinearOrderedRing
[same for semirings]

Then go through all usages of StrictLinearOrderedRing and see which can be relaxed to LinearOrderedRing (I bet it's a lot of them).

What do y'all think? Good idea? Or is it not worth the person-hours to refactor and review unless a mathematically relevant use for the distinction appears?

By concern with waiting is that we will rack up technical debt. For example, I am currently proving that a LinearOrderedRing R induces LinearOrderedRing on its localisations at S : Submonoid R. The right condition on S is S ≤ R⁰, but, since we are in a domain, this is equivalent to 0 ∉ S. I'm sure the "simpler" choice is being made all the time across Mathlib when LinearOrderedRing is used.

[Johan Commelin]

This sounds like a good idea indeed. Do you think that strictness should be a mixin?

class LinearOrderedRing -- aka BourbakiWikiNonstrictLinOrdRing
  ...

class IsStrict (R : Type) [LinearOrderedRing] : Prop where
  ...

[Artie Khovanov]

We can already mixin NoZeroDivisors. Will need to check if this still works for semirings, but I think it should.

[Artie Khovanov]

OK, for semirings we need the slightly stronger condition that a > 0 implies the map (a * ·) is injective.

[Artie Khovanov]

StrictOrderedFoo (where Foo extends Semiring) is also equivalent to (the conjunction of) the mixins PosMulReflectLT and MulPosReflectLT, so I guess we could have it be an alias for that? This would simplify Mathlib.Algebra.Order.Ring.Defs greatly by removing half the declarations.

[Artie Khovanov]

(By the way, we can't relax the base structure below Semiring because eg LinearOrderedCommMonoidWithZerorequires 0 to be the least element. I guess we could add OrderedNonUnitalSemiring for fun, but no further.)