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 often satisfies IsOrderedAddMonoid,
it usually does not satisfy IsOrderedRing.
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.
- 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
A class to encode that self-adjoint elements may be expressed as the
difference of nonnegative elements. This is satisfied by any type with a
NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint instance.
However, it can also be satisfied by continuous linear functionals equipped
with the intrinsic star operation.
This type class can be used to guarantee PositiveLinearMap is a StarHomClass.
- exists_nonneg_sub_nonneg {a : R} (ha : IsSelfAdjoint a) : ∃ (b : R) (c : R), 0 ≤ b ∧ 0 ≤ c ∧ a = b - c
Every self-adjoint element is the difference of nonnegative elements.
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.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.
Alias of IsSelfAdjoint.of_ge.
An alias of IsSelfAdjoint.of_nonneg for use with dot notation.
The combination (IsSelfAdjoint.star_eq <| .of_nonneg ·) for use with dot notation.
A star projection is non-negative in a star-ordered ring.
Alias of the reverse direction of IsSelfAdjoint.iff_of_le.
While IsSelfAdjoint.map assumes the map is star-preserving, this lemma instead assumes the
map is an order-preserving additive map from a space where self-adjoint elements can be expressed as
differences of nonnegative elemens, and whose codomain is a star-ordered ring. When such maps are
linear over ℂ, they are also star-preserving, and this lemma is used to establish that one by
splitting into real and imaginary parts.
Alias of IsSelfAdjoint.map'.
While IsSelfAdjoint.map assumes the map is star-preserving, this lemma instead assumes the
map is an order-preserving additive map from a space where self-adjoint elements can be expressed as
differences of nonnegative elemens, and whose codomain is a star-ordered ring. When such maps are
linear over ℂ, they are also star-preserving, and this lemma is used to establish that one by
splitting into real and imaginary parts.
For a star projection p, we have 0 ≤ p ≤ 1.
A star projection p is less than or equal to a star projection q when p * q = p.
A star projection p is less than or equal to a star projection q when q * p = p.