Holders Theorem

Stream: Is there code for X?

[Eric Paul]

Does mathlib have the following theorem of Holder (I couldn’t find it and just wanted to double check I hadn’t missed it):

An (left) ordered Archimedean group is isomorphic to a subgroup of the Reals under addition.

[Edward van de Meent]

wait, does that imply that Surreal numbers are isomorphic to a subgroup of the Reals?

[Edward van de Meent]

is that right?

[Yaël Dillies]

I don't think surreal numbers are archimedean?

[Kevin Buzzard]

I thought the surreal numbers have a much larger cardinality than the reals.

[Edward van de Meent]

surreals are a Field...

[Yaël Dillies]

That doesn't make them archimedean

[Edward van de Meent]

that's true... maybe i have a bad intuition for Surreals...

[Yaël Dillies]

I know some people were interested in Hölder's theorem a few years ago (@Yakov Pechersky, @Julian Berman was it you?) but I doubt anything came out of it

[Edward van de Meent]

ah, i think i see the problem... it is indeed not archimedian

[Edward van de Meent]

you can pick a combination like $\omega$ and $1$, and there is no $n$ such that $\omega \leq n \cdot 1$

[Julian Berman]

(Not me at least but that does sound like stuff Yakov has poked at I think)

[Yakov Pechersky]

I worked on Nakada's paper that ordered groups admit a linear order. Alex Best also had similar work iirc.

[Eric Paul]

Oh interesting. I’d be curious to look at this related work you guys have done if possible.

[Yakov Pechersky]

Mathlib 3 has a branch called pechersky/nakada

[Eric Paul]

Also, I wanted to double check that mathlib does not have ordered non-abelian groups.

As far as I could find there are only things like the following:
OrderedAddCommGroup
LinearOrderedAddCommGroup

I need linearly ordered groups that are not abelian as a big part of the result of Holder's theorem is that the group is in fact abelian.

Is there a reason mathlib doesn't already have non-abelian ordered groups?

[Damiano Testa]

My recollection is that, when it came up, no one had anything too specific that they wanted to do and hence they were not introduced.

[Eric Paul]

Eric Paul said:

Does mathlib have the following theorem of Holder (I couldn’t find it and just wanted to double check I hadn’t missed it):

An (left) ordered Archimedean group is isomorphic to a subgroup of the Reals under addition.

Finished a formalization of it, in the unlikely case someone else needs it

[Kevin Buzzard]

PR it in case someone does!