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)
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.of_nonneg_iff
).
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 ofStarOrderedRing
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.
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.of_nonneg_iff
.
Porting note: dropped an unneeded assumption
add_le_add_left : ∀ {x y}, x ≤ y → ∀ z, z + x ≤ z + y
- le_iff : ∀ (x y : R), x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun (s : R) => star s * s), y = x + p
characterization of the order in terms of the
StarRing
structure.
Instances
characterization of the order in terms of the StarRing
structure.
Equations
- StarOrderedRing.toOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯
Equations
- ⋯ = ⋯
Equations
- StarOrderedRing.toOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯
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.of_nonneg_iff
for a more convenient version.
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
.
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.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯