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 ofStarOrderedRingcould 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
StarRingstructure.
Instances
Equations
- StarOrderedRing.toOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯
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.
An alias of IsSelfAdjoint.of_nonneg for use with dot notation.
The combination (IsSelfAdjoint.star_eq <| .of_nonneg ·) for use with dot notation.