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 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.
- 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
StarRingstructure.
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.
Equations
- StarOrderedRing.ofLEIff h_le_iff = StarOrderedRing.mk (_ : ∀ (x y : R), x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p)
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.
Equations
- StarOrderedRing.ofNonnegIff h_add h_nonneg_iff = StarOrderedRing.mk (_ : ∀ (x y : R), x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p)
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.
Equations
- StarOrderedRing.ofNonnegIff' h_add h_nonneg_iff = StarOrderedRing.ofLEIff (_ : ∀ (a a_1 : R), a ≤ a_1 ↔ ∃ x, a_1 = a + star x * x)