LinearOrderedField with StarRing : TrivialStar

Stream: maths

[MohanadAhmed]

Is any of the following statements true:

Given a LinearOrderedField with StarRing can I either show it has a TrivialStar (Like R and Q) or it is a StarOrderedRing?
Or equivalently to number 1 as expressed by @Eric Wieser given a ring homomorphism that is involutive can we show that it is the identity map?

instance inst1 [LinearOrderedField R] [StarRing R] : TrivialStar R := sorry
instance inst2 [LinearOrderedField R] [StarRing R] : StarOrderedRing R := sorry
example [LinearOrderedField R] (f : R →+* R) (hf : Function.Involutive f) : f = RingHom.id R
:= sorry

[Kevin Buzzard]

How about R=Q(sqrt(2)) with the ordering coming from the embedding into the reals sending sqrt(2) to the positive real square root, and f is the function sending +sqrt(2) to -sqrt(2)?

[Eric Wieser]

Nice, in retrospect that's an obvious counterexample

[Kevin Buzzard]

in mathematics an awful lot of things are obvious in retrospect, it's a very P != NP place.

[MohanadAhmed]

If I understand this correctly, what you are saying is:

Let $R = \{ x : \mathbb{R} \quad | \quad x = a + b\sqrt{2}, a,b \in \mathbb{Q} \}$
Let $f(x) : R \to R := a + b\sqrt{2} \to a - b\sqrt{2}$
The $f$ is involutive but not trivial and the field is linearly ordered by embedding in $$\mathbb{R}$. So this kills 1 and 3. And for StarOrderedRing we will not be able to find $c + d\sqrt{2}$ such that $a + b\sqrt{2} = (c - d\sqrt{2})(c + d\sqrt{2}) = c^2 - 2d^2$ hence not a starOrderedRing.
Thanks

[Kevin Buzzard]

docs#StarOrderedRing

[Kevin Buzzard]

docs#StarRing

[Kevin Buzzard]

I don't really know all these star definitions but it's not a StarOrderedRing because the <= structure coming from the reals and the xx* structure coming from the star are totally unrelated.