# 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.

- star : R → R
- star_involutive : Function.Involutive star
- le_iff : ∀ (x y : R), x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s_1 => star s_1 * s_1) ∧ y = x + p
characterization of the order in terms of the

`StarRing`

structure.

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

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

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

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.