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

class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] extends StarRing : Type u

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

• star : R → R
• star_involutive : Function.Involutive star
• star_mul : ∀ (r s : R), star (r * s) = star s * star r
• star_add : ∀ (r s : R), star (r + s) = star r + star s
• 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.

instance StarOrderedRing.toOrderedAddCommMonoid {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] : OrderedAddCommMonoid R

Equations

• StarOrderedRing.toOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

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

Equations

• ⋯ = ⋯

instance StarOrderedRing.toOrderedAddCommGroup {R : Type u} [NonUnitalRing R] [PartialOrder R] [StarOrderedRing R] : OrderedAddCommGroup R

Equations

• StarOrderedRing.toOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯

@[reducible]

def StarOrderedRing.ofLEIff {R : Type u} [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.ofNonnegIff for a more convenient version.

Equations

• StarOrderedRing.ofLEIff h_le_iff = StarOrderedRing.mk ⋯

@[reducible]

def StarOrderedRing.ofNonnegIff {R : Type u} [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.

Equations

• StarOrderedRing.ofNonnegIff h_add h_nonneg_iff = StarOrderedRing.mk ⋯

@[reducible]

def StarOrderedRing.ofNonnegIff' {R : Type u} [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.

Equations

• StarOrderedRing.ofNonnegIff' h_add h_nonneg_iff = StarOrderedRing.ofLEIff ⋯

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem NonUnitalRingHom.map_le_map_of_map_star {R : Type u_2} {S : Type u_3} [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] [NonUnitalSemiring S] [PartialOrder S] [StarOrderedRing S] (f : R →ₙ+* S) (hf : ∀ (r : R), f (star r) = star (f r)) {x : R} {y : R} (hxy : x ≤ y) : f x ≤ f y

instance StarRingHomClass.instOrderHomClass {F : Type u_1} {R : Type u_2} {S : Type u_3} [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] [NonUnitalSemiring S] [PartialOrder S] [StarOrderedRing S] [FunLike F R S] [StarHomClass F R S] [NonUnitalRingHomClass F R S] : OrderHomClass F R S

Equations

• ⋯ = ⋯

instance StarRingHomClass.instOrderIsoClass {F : Type u_1} {R : Type u_2} {S : Type u_3} [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] [NonUnitalSemiring S] [PartialOrder S] [StarOrderedRing S] [EquivLike F R S] [StarHomClass F R S] [RingEquivClass F R S] : OrderIsoClass F R S

Equations

• ⋯ = ⋯

instance Nat.instStarOrderedRing : StarOrderedRing ℕ

Equations

• Nat.instStarOrderedRing = StarOrderedRing.mk Nat.instStarOrderedRing.proof_1