Error in MIL: "partial order" should be "total order"?

Stream: new members

[Martin Epstein]

I'm working through Mathematics In Lean and I believe I found a minor error. In section 7.2 : Algebraic Structures it is written

An ordered ring  consists of a ring together with a partial order on its elements...

This should say total order, no? The equality relation is a partial order and behaves the right way under addition and multiplication, but I don't think anyone would call an arbitrary ring with equality an ordered ring.

[Aaron Liu]

well docs#IsOrderedRing only assumes a partial order

[Aaron Liu]

to be an ordered ring you need 0 ≤ 1 so an arbitrary ring with equality doesn't count (unless you have the trivial ring)

[Aaron Liu]

and the complex numbers are a partially ordered ring in the ComplexOrder scope

[Aaron Liu]

but they aren't a totally ordered ring since -1 is a square

[Martin Epstein]

Ah, well in that case the mistake in MIL is that the 0 ≤ 1 requirement is missing. The full definition given is:
An ordered ring (R, +, 0, -, ·, 1, ≤) consists of a ring together with a partial order on its elements, such that a ≤ b implies a + c ≤ b + c for every a, b, and c in R, and 0 ≤ a and 0 ≤ b implies 0 ≤ ab for every a and b in R.

[Aaron Liu]

We got rid of the "ordered ring" typeclass, now we have "the order is compatible with the ring structure" typeclass

[Aaron Liu]

This makes it a lot easier to talk about stuff if you want to upgrade the order or upgrade the ring

[Kenny Lau]

Can you link to the section?

[Aaron Liu]

so now the module docstring is outdated and I guess mil might be outdated too

[Kenny Lau]

Martin Epstein said:

This should say total order, no? The equality relation is a partial order and behaves the right way under addition and multiplication, but I don't think anyone would call an arbitrary ring with equality an ordered ring.

I wouldn't call this an "error". For many typeclasses you can find "weird" objects, that doesn't mean the typeclass shouldn't exist.

[Martin Epstein]

Kenny Lau said:

Can you link to the section?

Sure: https://leanprover-community.github.io/mathematics_in_lean/C07_Structures.html#algebraic-structures

[Kenny Lau]

For example, the "zero ring" is also very weird, it only maps to itself, and everything maps to it. but it's still a ring.

[Martin Epstein]

True, but Aaron's link to the docs confirms my suspicion (although for a different reason than I first thought). An arbitrary ring is not ordered under the equality relation since an ordered ring must satisfy 0 ≤ 1.