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 of StarOrderedRing could 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.

theorem smul_mem_closure_star_mul {R : Type u_1} {A : Type u_2} [Semiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] {r : R} (hr : r ∈ AddSubmonoid.closure (Set.range fun (s : R) => star s * s)) {a : A} (ha : a ∈ AddSubmonoid.closure (Set.range fun (s : A) => star s * s)) : r • a ∈ AddSubmonoid.closure (Set.range fun (s : A) => star s * s)

class StarOrderedRing (R : Type u_3) [NonUnitalSemiring R] [PartialOrder R] [StarRing R] : Prop

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 StarRing structure.

theorem StarOrderedRing.of_le_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] (h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s) : StarOrderedRing R

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.

@[instance 100]

instance StarOrderedRing.toIsOrderedAddMonoid {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] : IsOrderedAddMonoid R

@[instance 100]

instance StarOrderedRing.toExistsAddOfLE {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] : ExistsAddOfLE R

theorem StarOrderedRing.nonneg_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun (s : R) => star s * s)

theorem StarOrderedRing.pos_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : 0 < x ↔ x ≠ 0 ∧ x ∈ AddSubmonoid.closure (Set.range fun (s : R) => star s * s)

theorem StarOrderedRing.lt_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x y : R} [IsCancelAdd R] : x < y ↔ ∃ (p : R), p ≠ 0 ∧ p ∈ AddSubmonoid.closure (Set.range fun (s : R) => star s * s) ∧ y = x + p

theorem StarOrderedRing.of_nonneg_iff {R : Type u_1} [NonUnitalRing R] [PartialOrder R] [StarRing R] (h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) (h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun (s : R) => star s * s)) : StarOrderedRing 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 in the AddSubmonoid generated by star s * s for s : R.

theorem StarOrderedRing.of_nonneg_iff' {R : Type u_1} [NonUnitalRing R] [PartialOrder R] [StarRing R] (h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) (h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ (s : R), x = star s * s) : StarOrderedRing 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.

theorem IsSelfAdjoint.mono {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y

theorem IsSelfAdjoint.of_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x

theorem LE.le.isSelfAdjoint {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x

An alias of IsSelfAdjoint.of_nonneg for use with dot notation.

theorem LE.le.star_eq {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} (hx : 0 ≤ x) : star x = x

The combination (IsSelfAdjoint.star_eq <| .of_nonneg ·) for use with dot notation.

@[simp]

theorem star_mul_self_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (r : R) : 0 ≤ star r * r

@[simp]

theorem mul_star_self_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (r : R) : 0 ≤ r * star r

theorem IsSelfAdjoint.mul_self_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a * a

theorem IsStarProjection.nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p : R} (hp : IsStarProjection p) : 0 ≤ p

A star projection is non-negative in a star-ordered ring.

theorem star_left_conjugate_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c

@[deprecated star_left_conjugate_nonneg (since := "2025-10-20")]

theorem conjugate_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c

Alias of star_left_conjugate_nonneg.

theorem star_right_conjugate_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c

@[deprecated star_right_conjugate_nonneg (since := "2025-10-20")]

theorem conjugate_nonneg' {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c

Alias of star_right_conjugate_nonneg.

theorem IsSelfAdjoint.conjugate_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a) {c : R} (hc : IsSelfAdjoint c) : 0 ≤ c * a * c

theorem conjugate_nonneg_of_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a) {c : R} (hc : 0 ≤ c) : 0 ≤ c * a * c

theorem star_left_conjugate_le_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c

@[deprecated star_left_conjugate_le_conjugate (since := "2025-10-20")]

theorem conjugate_le_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c

Alias of star_left_conjugate_le_conjugate.

theorem star_right_conjugate_le_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c

@[deprecated star_right_conjugate_le_conjugate (since := "2025-10-20")]

theorem conjugate_le_conjugate' {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c

Alias of star_right_conjugate_le_conjugate.

theorem IsSelfAdjoint.conjugate_le_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a ≤ b) {c : R} (hc : IsSelfAdjoint c) : c * a * c ≤ c * b * c

theorem conjugate_le_conjugate_of_nonneg {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a ≤ b) {c : R} (hc : 0 ≤ c) : c * a * c ≤ c * b * c

@[simp]

theorem star_le_star_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x y : R} : star x ≤ star y ↔ x ≤ y

@[simp]

theorem star_lt_star_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x y : R} : star x < star y ↔ x < y

theorem star_le_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x y : R} : star x ≤ y ↔ x ≤ star y

theorem star_lt_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x y : R} : star x < y ↔ x < star y

@[simp]

theorem star_nonneg_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : 0 ≤ star x ↔ 0 ≤ x

@[simp]

theorem star_nonpos_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : star x ≤ 0 ↔ x ≤ 0

@[simp]

theorem star_pos_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : 0 < star x ↔ 0 < x

@[simp]

theorem star_neg_iff {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : star x < 0 ↔ x < 0

theorem star_left_conjugate_lt_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) : star c * a * c < star c * b * c

@[deprecated star_left_conjugate_lt_conjugate (since := "2025-10-20")]

theorem conjugate_lt_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) : star c * a * c < star c * b * c

Alias of star_left_conjugate_lt_conjugate.

theorem star_right_conjugate_lt_conjugate {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) : c * a * star c < c * b * star c

@[deprecated star_right_conjugate_lt_conjugate (since := "2025-10-20")]

theorem conjugate_lt_conjugate' {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) : c * a * star c < c * b * star c

Alias of star_right_conjugate_lt_conjugate.

theorem star_left_conjugate_pos {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) : 0 < star c * a * c

@[deprecated star_left_conjugate_pos (since := "2025-10-20")]

theorem conjugate_pos {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) : 0 < star c * a * c

Alias of star_left_conjugate_pos.

theorem star_right_conjugate_pos {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) : 0 < c * a * star c

@[deprecated star_right_conjugate_pos (since := "2025-10-20")]

theorem conjugate_pos' {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) : 0 < c * a * star c

Alias of star_right_conjugate_pos.

theorem star_mul_self_pos {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < star x * x

theorem mul_star_self_pos {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < x * star x

instance instZeroLEOneClass {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] : ZeroLEOneClass R

@[simp]

theorem one_le_star_iff {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : 1 ≤ star x ↔ 1 ≤ x

@[simp]

theorem star_le_one_iff {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : star x ≤ 1 ↔ x ≤ 1

@[simp]

theorem one_lt_star_iff {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : 1 < star x ↔ 1 < x

@[simp]

theorem star_lt_one_iff {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} : star x < 1 ↔ x < 1

theorem IsSelfAdjoint.sq_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a ^ 2

theorem IsUnit.star_right_conjugate_nonneg_iff {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {u x : R} (hu : IsUnit u) : 0 ≤ u * x * star u ↔ 0 ≤ x

theorem IsUnit.star_left_conjugate_nonneg_iff {R : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {u x : R} (hu : IsUnit u) : 0 ≤ star u * x * u ↔ 0 ≤ x

instance MulOpposite.instStarOrderedRing {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] : StarOrderedRing Rᵐᵒᵖ

instance instIsOrderedModule {R : Type u_1} {A : Type u_2} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] : IsOrderedModule R A

instance instPosSMulStrictMono {R : Type u_1} {A : Type u_2} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsDomain R] [IsCancelAdd A] [Module.IsTorsionFree R A] : PosSMulStrictMono R A

instance instIsStrictOrderedModuleOfIsCancelAdd {R : Type u_1} {A : Type u_2} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsDomain R] [IsCancelAdd A] [Module.IsTorsionFree R A] [IsCancelAdd R] : IsStrictOrderedModule R A

theorem NonUnitalStarRingHom.map_le_map_of_map_star {R : Type u_4} {S : Type u_5} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring S] [PartialOrder S] [StarRing S] [StarOrderedRing S] (f : R →⋆ₙ+* S) {x y : R} (hxy : x ≤ y) : f x ≤ f y

@[instance 100]

instance StarRingHomClass.instOrderHomClass {F : Type u_3} {R : Type u_4} {S : Type u_5} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [NonUnitalSemiring S] [PartialOrder S] [StarRing S] [FunLike F R S] [StarOrderedRing R] [StarOrderedRing S] [NonUnitalRingHomClass F R S] [NonUnitalStarRingHomClass F R S] : OrderHomClass F R S

@[instance 100]

instance StarRingEquivClass.instOrderIsoClass {F : Type u_3} {R : Type u_4} {S : Type u_5} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring S] [PartialOrder S] [StarRing S] [StarOrderedRing S] [EquivLike F R S] [StarRingEquivClass F R S] : OrderIsoClass F R S

instance Nat.instStarOrderedRing : StarOrderedRing ℕ

theorem IsStarProjection.one_sub_nonneg {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p : R} (hp : IsStarProjection p) : 0 ≤ 1 - p

theorem IsStarProjection.le_one {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p : R} (hp : IsStarProjection p) : p ≤ 1

theorem IsStarProjection.mem_Icc {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p : R} (hp : IsStarProjection p) : p ∈ Set.Icc 0 1

For a star projection p, we have 0 ≤ p ≤ 1.

theorem IsStarProjection.le_of_mul_eq_left {R : Type u_1} [NonUnitalRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) : p ≤ q

A star projection p is less than or equal to a star projection q when p * q = p.

theorem IsStarProjection.le_of_mul_eq_right {R : Type u_1} [NonUnitalRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : q * p = p) : p ≤ q

A star projection p is less than or equal to a star projection q when q * p = p.