Commutative star-ordered rings are ordered rings

A noncommutative star-ordered ring is generally not an ordered ring. Indeed, in a star-ordered ring, nonnegative elements are self-adjoint, but the product of self-adjoint elements is self-adjoint if and only if they commute. Therefore, a necessary condition for a star-ordered ring to be an ordered ring is that all nonnegative elements commute. Consequently, if a star-ordered ring is spanned by it nonnegative elements (as is the case for C⋆-algebras) and it is also an ordered ring, then it is commutative.

In this file we prove the converse: a commutative star-ordered ring is an ordered ring.

@[reducible]

def StarOrderedRing.toOrderedCommSemiring (R : Type u_1) [CommSemiring R] [PartialOrder R] [StarOrderedRing R] : OrderedCommSemiring R

A commutative star-ordered semiring is an ordered semiring.

This is not registered as an instance because it introduces a type class loop between CommSemiring and OrderedCommSemiring, and it seem loops still cause issues sometimes.

See note [reducible non-instances].

Equations

• StarOrderedRing.toOrderedCommSemiring R = OrderedCommSemiring.mk (_ : ∀ (a b : R), a * b = b * a)

@[reducible]

def StarOrderedRing.toOrderedCommRing (R : Type u_1) [CommRing R] [PartialOrder R] [StarOrderedRing R] : OrderedCommRing R

A commutative star-ordered ring is an ordered ring.

This is not registered as an instance because it introduces a type class loop between CommSemiring and OrderedCommSemiring, and it seem loops still cause issues sometimes.

See note [reducible non-instances].

Equations

• StarOrderedRing.toOrderedCommRing R = OrderedCommRing.mk (_ : ∀ (a b : R), a * b = b * a)