Johan Commelin (Nov 26 2019 at 15:20):
Question that came up in #1744:
Are there archimedean linearly ordered semirings that are not commutative?
Chris Hughes (Nov 26 2019 at 18:40):
I think this works.
free_semiring bool and say
ff < tt and the free monoid
M generated by
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
Johan Commelin (Nov 26 2019 at 20:16):
Ok, funny. Thanks for this example!
Last updated: May 11 2021 at 16:22 UTC