Documentation

Mathlib.Algebra.Order.Ring.Star

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.

source
@[reducible]
def StarOrderedRing.toOrderedCommSemiring (R : Type u_1) [CommSemiring R] [PartialOrder R] [StarRing 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
Instances For
    source
    @[reducible]
    def StarOrderedRing.toOrderedCommRing (R : Type u_1) [CommRing R] [PartialOrder R] [StarRing 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
    Instances For