Star ordered rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the class star_ordered_ring R, which says that the order on R respects the
star operation, i.e. an element r is nonnegative iff it is in the add_submonoid 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 star_ordered_ring instance for ℚ), and more closely resembles the
literature (see the seminal paper The positive cone in Banach algebras)
In order to accodomate non_unital_semiring R, we actually don't characterize nonnegativity, but
rather the entire ≤ relation with star_ordered_ring.le_iff. However, notice that when R is a
non_unital_ring, these are equivalent (see star_ordered_ring.nonneg_iff and
star_ordered_ring.of_nonneg_iff).
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 ofstar_ordered_ringcould 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.
- to_star_ring : star_ring R
- add_le_add_left : ∀ (a b : R), a ≤ b → ∀ (c : R), c + a ≤ c + b
- le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (p : R), p ∈ add_submonoid.closure (set.range (λ (s : R), has_star.star s * s)) ∧ y = x + p
An ordered *-ring is a ring which is both an ordered_add_comm_group and a *-ring,
and the nonnegative elements constitute precisely the add_submonoid generated by
elements of the form star s * s.
If you are working with a non_unital_ring and not a non_unital_semiring, it may be more
convenient do declare instances using star_ordered_ring.of_nonneg_iff'.
Instances of this typeclass
Instances of other typeclasses for star_ordered_ring
- star_ordered_ring.has_sizeof_inst
Equations
- star_ordered_ring.to_ordered_add_comm_monoid = {add := non_unital_semiring.add (show non_unital_semiring R, from _inst_1), add_assoc := _, zero := non_unital_semiring.zero (show non_unital_semiring R, from _inst_1), zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul (show non_unital_semiring R, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le (show partial_order R, from _inst_2), lt := partial_order.lt (show partial_order R, from _inst_2), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
Equations
- star_ordered_ring.to_ordered_add_comm_group = {add := non_unital_ring.add (show non_unital_ring R, from _inst_1), add_assoc := _, zero := non_unital_ring.zero (show non_unital_ring R, from _inst_1), zero_add := _, add_zero := _, nsmul := non_unital_ring.nsmul (show non_unital_ring R, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg (show non_unital_ring R, from _inst_1), sub := non_unital_ring.sub (show non_unital_ring R, from _inst_1), sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul (show non_unital_ring R, from _inst_1), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (show partial_order R, from _inst_2), lt := partial_order.lt (show partial_order R, from _inst_2), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
To construct a star_ordered_ring 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 add_submonoid.closure_induction when creating those instances.
If you are working with a non_unital_ring and not a non_unital_semiring, see
star_ordered_ring.of_nonneg_iff for a more convenient version.
Equations
- star_ordered_ring.of_le_iff h_add h_le_iff = {to_star_ring := {to_star_semigroup := star_ring.to_star_semigroup _inst_3, star_add := _}, add_le_add_left := h_add, le_iff := _}
When R is a non-unital ring, to construct a star_ordered_ring instance it suffices to
show that the nonnegative elements are precisely those elements in the add_submonoid generated
by star s * s for s : R.
Equations
- star_ordered_ring.of_nonneg_iff h_add h_nonneg_iff = {to_star_ring := {to_star_semigroup := star_ring.to_star_semigroup _inst_3, star_add := _}, add_le_add_left := h_add, le_iff := _}
When R is a non-unital ring, to construct a star_ordered_ring 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 add_submonoid.closure_induction when creating those
instances.
Equations
- star_ordered_ring.of_nonneg_iff' h_add h_nonneg_iff = star_ordered_ring.of_le_iff h_add _