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

source

@[class]

structure star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R] :

Type u

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

source

@[protected, instance]

def star_ordered_ring.to_ordered_add_comm_monoid {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] :

ordered_add_comm_monoid R

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 := _}

source

@[protected, instance]

def star_ordered_ring.to_has_exists_add_of_le {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] :

has_exists_add_of_le R

source

@[protected, instance]

def star_ordered_ring.to_ordered_add_comm_group {R : Type u} [non_unital_ring R] [partial_order R] [star_ordered_ring R] :

ordered_add_comm_group R

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 := _}

source

@[reducible]

def star_ordered_ring.of_le_iff {R : Type u} [non_unital_semiring R] [partial_order R] [star_ring R] (h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) (h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + has_star.star s * s) :

star_ordered_ring R

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 := _}

source

@[reducible]

def star_ordered_ring.of_nonneg_iff {R : Type u} [non_unital_ring R] [partial_order R] [star_ring R] (h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) (h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range (λ (s : R), has_star.star s * s))) :

star_ordered_ring R

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 := _}

source

@[reducible]

def star_ordered_ring.of_nonneg_iff' {R : Type u} [non_unital_ring R] [partial_order R] [star_ring R] (h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) (h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ (s : R), x = has_star.star s * s) :

star_ordered_ring R

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 _

source

theorem star_ordered_ring.nonneg_iff {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {x : R} :

0 ≤ x ↔ x ∈ add_submonoid.closure (set.range (λ (s : R), has_star.star s * s))

source

theorem star_mul_self_nonneg {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] (r : R) :

0 ≤ has_star.star r * r

source

theorem star_mul_self_nonneg' {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] (r : R) :

0 ≤ r * has_star.star r

source

theorem conjugate_nonneg {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {a : R} (ha : 0 ≤ a) (c : R) :

0 ≤ has_star.star c * a * c

source

theorem conjugate_nonneg' {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {a : R} (ha : 0 ≤ a) (c : R) :

0 ≤ c * a * has_star.star c

source

theorem conjugate_le_conjugate {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {a b : R} (hab : a ≤ b) (c : R) :

has_star.star c * a * c ≤ has_star.star c * b * c

source

theorem conjugate_le_conjugate' {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {a b : R} (hab : a ≤ b) (c : R) :

c * a * has_star.star c ≤ c * b * has_star.star c