Documentation

Mathlib.Algebra.Star.Order

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 #

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

Instances
    Equations
    theorem 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) :

    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.

    theorem 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)) :

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

    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 conjugate_nonneg {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing 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] [StarRing 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] [StarRing 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] [StarRing 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] [StarRing 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] [StarRing R] [StarOrderedRing R] {x : R} {y : R} :
    star x < star y x < y
    theorem star_le_iff {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} {y : R} :
    star x y x star y
    theorem star_lt_iff {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing 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] [StarRing R] [StarOrderedRing R] {x : R} :
    0 star x 0 x
    @[simp]
    theorem star_nonpos_iff {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    star x 0 x 0
    @[simp]
    theorem star_pos_iff {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    0 < star x 0 < x
    @[simp]
    theorem star_neg_iff {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    star x < 0 x < 0
    theorem IsSelfAdjoint.mono {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} {y : R} (h : x y) (hx : IsSelfAdjoint x) :
    @[simp]
    theorem one_le_star_iff {R : Type u} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    1 star x 1 x
    @[simp]
    theorem star_le_one_iff {R : Type u} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    star x 1 x 1
    @[simp]
    theorem one_lt_star_iff {R : Type u} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    1 < star x 1 < x
    @[simp]
    theorem star_lt_one_iff {R : Type u} [Semiring R] [PartialOrder R] [StarRing 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] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring S] [PartialOrder S] [StarRing 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