mathlib3 documentation

algebra.star.order

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 #

@[class]

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
@[protected, instance]
Equations
@[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) :

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
@[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))) :

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
@[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) :

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
theorem conjugate_nonneg {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {a : R} (ha : 0 a) (c : R) :
theorem conjugate_nonneg' {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {a : R} (ha : 0 a) (c : R) :
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) :
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) :