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.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][kelleyVaught1953]). 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
- ⋯ = ⋯
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
- ⋯ = ⋯