Why linear_ordered_ring

Stream: general

[Yaël Dillies]

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]

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
• Add all missing noncommutative versions

[Alex J. Best]

I guess interesting doesn't have a precise definition, but it seems examples of linear_ordered_ring that are not linear_ordered_comm_rings 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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

or slower

[Yaël Dillies]

Actually, they already exist: docs#covariant_class

[Mario Carneiro]

or bigger / harder to debug and understand

[Kevin Buzzard]

eg docs#covariant_class :-/

[Mario Carneiro]

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

[Mario Carneiro]

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]

So are we leaning towards deleting linear_ordered_ring?

[Kevin Buzzard]

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

[Junyan Xu]

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]

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.