# Zulip Chat Archive

## Stream: general

### Topic: Why linear_ordered_ring

#### Yaël Dillies (Jun 28 2022 at 10:00):

There is this general fact that linearly ordered algebraic structures have to be commutative to be interesting. For example, we do not have non commutative versions of linear ordered:

- monoids (no
`linear_ordered_monoid`

) - additive monoids (no
`linear_ordered_add_monoid`

) - semirings (docs#linear_ordered_semiring assumes commutativity)
- division rings (no
`linear_ordered_division_ring`

)

and same all over again for canonically ordered stuff. The only exception is docs#linear_ordered_ring vs docs#linear_ordered_comm_ring and, unsurprisingly, all instances of the former are covered by instances of the latter. Should we thus get rid of it?

#### Yaël Dillies (Jun 28 2022 at 10:02):

I see three options:

- Get rid of
`linear_ordered_ring`

- Remove
`_comm`

from all`linear_ordered_`

typeclasses names for consistency with`linear_ordered_semiring`

- Add
`_comm`

to all`linear_ordered_`

typeclasses names for consistency with`linear_ordered_comm_monoid`

- Remove
- Add all missing noncommutative versions

#### Alex J. Best (Jun 28 2022 at 10:44):

I guess interesting doesn't have a precise definition, but it seems examples of `linear_ordered_ring`

that are not `linear_ordered_comm_ring`

s do exist, at least in math if not in `mathlib`

, https://math.stackexchange.com/questions/621111/existence-of-non-commutative-ordered-ring/621121#621121 (unless I'm messing up translating mathlib speak to math terminology again...).

#### Yaël Dillies (Jun 28 2022 at 10:48):

I perfectly agree that they exist. My problem with the current situation is that rings are treated differently from quite literally everything else for no apparent reason (and this causes pain when trying to generalize statements). I'm happy to normalize either way.

#### Kevin Buzzard (Jun 28 2022 at 10:48):

I'm not sure "one exercise in a textbook" counts as good enough reason for "mathlib support". If someone really wants them they can just roll their own.

#### Junyan Xu (Jun 28 2022 at 15:20):

There is this general fact that linearly ordered algebraic structures have to be commutative to be interesting.

Wait until you see https://en.wikipedia.org/wiki/Linearly_ordered_group (left/right orderability)

Fairly recent book: https://www.amazon.com/Ordered-Topology-Graduate-Studies-Mathematics/dp/1470431068

So I think we should go with the option "Add all missing noncommutative versions"

#### Kevin Buzzard (Jun 28 2022 at 18:31):

I think we should go with that option if and only if it doesn't make working with the commutative options much harder than right now -- if all of a sudden there is some defeq issues with a left ordering not being defeq to a right ordering -- problems which don't even exist right now -- then this is perhaps an issue. Note that many of the results on that Wikipedia page are for the abelian case.

#### Yaël Dillies (Jun 28 2022 at 20:54):

There's always only one ordering, right? The question is whether it left- or right-preserves addition/multiplication.

#### Kevin Buzzard (Jun 28 2022 at 21:14):

Oh ok, I'm just saying that I'm not convinced that this is important and if it makes things which were fine, harder, then it's an argument against.

#### Mario Carneiro (Jun 28 2022 at 21:14):

or slower

#### Yaël Dillies (Jun 28 2022 at 21:15):

Actually, they already exist: docs#covariant_class

#### Mario Carneiro (Jun 28 2022 at 21:15):

or bigger / harder to debug and understand

#### Kevin Buzzard (Jun 28 2022 at 21:15):

eg docs#covariant_class :-/

#### Mario Carneiro (Jun 28 2022 at 21:15):

I'm generally opposed to adding new typeclasses without good reason

#### Mario Carneiro (Jun 28 2022 at 21:16):

where good reason means at least that it is needed to prove a theorem which isn't directly related to noncommutative ordered whatevers

#### Yaël Dillies (Jun 28 2022 at 21:18):

So are we leaning towards deleting `linear_ordered_ring`

?

#### Kevin Buzzard (Jun 28 2022 at 21:23):

I'm not saying that, I'm just saying "try not to make things worse"

#### Junyan Xu (Jun 28 2022 at 22:57):

where good reason means at least that it is needed to prove a theorem which isn't directly related to noncommutative ordered whatevers

The book I linked above mentioned the solution (not the first one) of the Hanna Neumann conjecture by Mineyev which was an Annals paper. As said in the abstract, the paper established a certain result for arbitrary left-orderable groups, and applies it to free groups, which are left-orderable.

However the terminology "orderable" suggests the existence of many orderings without a canonical choice, as is often the case, so I'm not sure if typeclasses are the right mechanism to deal with them. But like we need docs#upgraded_polish_space to choose a complete metric on a Polish space, I expect we also need to endow the group with a linear order when working with left/bi-orderable groups.

#### Kyle Miller (Jul 19 2022 at 15:29):

Orderability of groups is important in 3-manifold topology. One reference is https://arxiv.org/pdf/1205.0202.pdf (take a look at pages 36 and 69 for some big flowcharts). A result on the first flowchart is that if $N$ is an irreducible compact orientable 3-manifold with empty or toroidal boundary whose fundamental group is neither finite nor solvable, then if $N$ is not hyperbolic there is a finite-sheeted cover $N'$ of $N$ whose fundamental group is left-orderable. The second flowchart gives additionally that if $N$ has a JSJ decomposition with at least one hyperbolic component then there is a finite-sheeted cover $N'$ of $N$ whose fundamental group is bi-orderable.

In the vein of Kaplansky's conjectures, it's known that if $G$ is a left-orderable torsion-free group then its group algebra has no zero divisors.

Left orderability has something to do with whether a 3-manifold has a co-orientable taut foliation, and there's a conjecture that irreducible rational homology spheres are L-spaces iff their fundamental group is not left orderable.

Last updated: Dec 20 2023 at 11:08 UTC