(non?)commutative linear ordered semirings

Stream: maths

[Johan Commelin]

Question that came up in #1744:

Are there archimedean linearly ordered semirings that are not commutative?

[Chris Hughes]

I think this works.

Use free_semiring bool and say ff < tt and the free monoid M generated by tt and ff can be linearly ordered lexicographically (I think this is the ordinal 2^omega, short words are always smaller than big words, so not quite the dictionary order). If an indexing set M is linearly ordered, then M ->_0 nat is linearly ordered lexicographically, so you can linearly order the free_semiring (you compare the coefficient of the biggest element of M for which the coefficients differ). I think this satisfies all the axioms, but some of the multiplication ones would be messy to verify. The multiplication axioms for ordered rings seem much simpler than for linear ordered semirings, I'd be quite confident about satisfying those with free_ring bool

[Johan Commelin]

Ok, funny. Thanks for this example!