# Documentation

Mathlib.Algebra.Star.Order

# Star ordered rings #

We define the class StarOrderedRing R, which says that the order on R respects the star operation, i.e. an element r is nonnegative iff it is in the AddSubmonoid 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 StarOrderedRing instance for ℚ), and more closely resembles the literature (see the seminal paper [The positive cone in Banach algebras][kelleyVaught1953])

In order to accommodate NonUnitalSemiring R, we actually don't characterize nonnegativity, but rather the entire ≤ relation with StarOrderedRing.le_iff. However, notice that when R is a NonUnitalRing, these are equivalent (see StarOrderedRing.nonneg_iff and StarOrderedRing.ofNonnegIff).

It is important to note that while a StarOrderedRing is an OrderedAddCommMonoid it is often not an OrderedSemiring.

## 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 StarOrderedRing could be defined for this case (again, see [The positive cone in Banach algebras][kelleyVaught1953]). Note that the current definition has the advantage of not requiring a topology.
class StarOrderedRing (R : Type u) [] extends :

An ordered *-ring is a *ring with a partial order such that the nonnegative elements constitute precisely the AddSubmonoid generated by elements of the form star s * s.

If you are working with a NonUnitalRing and not a NonUnitalSemiring, it may be more convenient to declare instances using StarOrderedRing.ofNonnegIff'.

Porting note: dropped an unneeded assumption add_le_add_left : ∀ {x y}, x ≤ y → ∀ z, z + x ≤ z + y

Instances
@[reducible]
def StarOrderedRing.ofLEIff {R : Type u} [] [] (h_le_iff : ∀ (x y : R), x y s, y = x + star s * s) :

To construct a StarOrderedRing 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 AddSubmonoid.closure_induction when creating those instances.

If you are working with a NonUnitalRing and not a NonUnitalSemiring, see StarOrderedRing.ofNonnegIff for a more convenient version.

Instances For
@[reducible]
def StarOrderedRing.ofNonnegIff {R : Type u} [] [] [] (h_add : ∀ {x y : R}, x y∀ (z : R), z + x z + y) (h_nonneg_iff : ∀ (x : R), 0 x x AddSubmonoid.closure (Set.range fun s => star s * s)) :

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

Instances For
@[reducible]
def StarOrderedRing.ofNonnegIff' {R : Type u} [] [] [] (h_add : ∀ {x y : R}, x y∀ (z : R), z + x z + y) (h_nonneg_iff : ∀ (x : R), 0 x s, x = star s * s) :

When R is a non-unital ring, to construct a StarOrderedRing 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 AddSubmonoid.closure_induction when creating those instances.

Instances For
theorem StarOrderedRing.nonneg_iff {R : Type u} [] [] {x : R} :
theorem star_mul_self_nonneg {R : Type u} [] [] (r : R) :
0 star r * r
theorem star_mul_self_nonneg' {R : Type u} [] [] (r : R) :
0 r * star r
theorem conjugate_nonneg {R : Type u} [] [] {a : R} (ha : 0 a) (c : R) :
0 star c * a * c
theorem conjugate_nonneg' {R : Type u} [] [] {a : R} (ha : 0 a) (c : R) :
0 c * a * star c
theorem conjugate_le_conjugate {R : Type u} [] [] {a : R} {b : R} (hab : a b) (c : R) :
star c * a * c star c * b * c
theorem conjugate_le_conjugate' {R : Type u} [] [] {a : R} {b : R} (hab : a b) (c : R) :
c * a * star c c * b * star c