# mathlib3documentation

algebra.star.order

# Star ordered rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the class star_ordered_ring R, which says that the order on R respects the star operation, i.e. an element r is nonnegative iff it is in the add_submonoid generated by elements of the form star s * s. In many cases, including all C⋆-algebras, this can be reduced to 0 ≤ r ↔ ∃ s, r = star s * s. However, this generality is slightly more convenient (e.g., it allows us to register a star_ordered_ring instance for ℚ), and more closely resembles the literature (see the seminal paper The positive cone in Banach algebras)

In order to accodomate non_unital_semiring R, we actually don't characterize nonnegativity, but rather the entire ≤ relation with star_ordered_ring.le_iff. However, notice that when R is a non_unital_ring, these are equivalent (see star_ordered_ring.nonneg_iff and star_ordered_ring.of_nonneg_iff).

## TODO #

• In a Banach star algebra without a well-defined square root, the natural ordering is given by the positive cone which is the closure of the sums of elements star r * r. A weaker version of star_ordered_ring could be defined for this case (again, see The positive cone in Banach algebras). Note that the current definition has the advantage of not requiring a topology.
@[class]
structure star_ordered_ring (R : Type u)  :

An ordered *-ring is a ring which is both an ordered_add_comm_group and a *-ring, and the nonnegative elements constitute precisely the add_submonoid generated by elements of the form star s * s.

If you are working with a non_unital_ring and not a non_unital_semiring, it may be more convenient do declare instances using star_ordered_ring.of_nonneg_iff'.

Instances of this typeclass
Instances of other typeclasses for star_ordered_ring
• star_ordered_ring.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[reducible]
def star_ordered_ring.of_le_iff {R : Type u} [star_ring R] (h_add : {x y : R}, x y (z : R), z + x z + y) (h_le_iff : (x y : R), x y (s : R), y = x + ) :

To construct a star_ordered_ring instance it suffices to show that x ≤ y if and only if y = x + star s * s for some s : R.

This is provided for convenience because it holds in some common scenarios (e.g.,ℝ≥0, C(X, ℝ≥0)) and obviates the hassle of add_submonoid.closure_induction when creating those instances.

If you are working with a non_unital_ring and not a non_unital_semiring, see star_ordered_ring.of_nonneg_iff for a more convenient version.

Equations
@[reducible]
def star_ordered_ring.of_nonneg_iff {R : Type u} [star_ring R] (h_add : {x y : R}, x y (z : R), z + x z + y) (h_nonneg_iff : (x : R), 0 x x add_submonoid.closure (set.range (λ (s : R), * s))) :

When R is a non-unital ring, to construct a star_ordered_ring instance it suffices to show that the nonnegative elements are precisely those elements in the add_submonoid generated by star s * s for s : R.

Equations
@[reducible]
def star_ordered_ring.of_nonneg_iff' {R : Type u} [star_ring R] (h_add : {x y : R}, x y (z : R), z + x z + y) (h_nonneg_iff : (x : R), 0 x (s : R), x = ) :

When R is a non-unital ring, to construct a star_ordered_ring instance it suffices to show that the nonnegative elements are precisely those elements of the form star s * s for s : R.

This is provided for convenience because it holds in many common scenarios (e.g.,ℝ, ℂ, or any C⋆-algebra), and obviates the hassle of add_submonoid.closure_induction when creating those instances.

Equations
• h_nonneg_iff = _
theorem star_ordered_ring.nonneg_iff {R : Type u} {x : R} :
0 x x add_submonoid.closure (set.range (λ (s : R), * s))
theorem star_mul_self_nonneg {R : Type u} (r : R) :
0
theorem star_mul_self_nonneg' {R : Type u} (r : R) :
0
theorem conjugate_nonneg {R : Type u} {a : R} (ha : 0 a) (c : R) :
0 * c
theorem conjugate_nonneg' {R : Type u} {a : R} (ha : 0 a) (c : R) :
0 c * a *
theorem conjugate_le_conjugate {R : Type u} {a b : R} (hab : a b) (c : R) :
* c * c
theorem conjugate_le_conjugate' {R : Type u} {a b : R} (hab : a b) (c : R) :
c * a * c * b *