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

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

Porting note: dropped an unneeded assumption add_le_add_left : ∀ {x y}, x ≤ y → ∀ z, z + x ≤ z + y

Instances
    theorem StarOrderedRing.le_iff {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [self : StarOrderedRing R] (x : R) (y : R) :
    x y pAddSubmonoid.closure (Set.range fun (s : R) => star s * s), y = x + p

    characterization of the order in terms of the StarRing structure.

    @[instance 100]
    Equations
    @[instance 100]
    Equations
    • =
    @[instance 100]
    Equations
    theorem StarOrderedRing.of_le_iff {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.of_nonneg_iff for a more convenient version.

    theorem StarOrderedRing.of_nonneg_iff {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.of_nonneg_iff' {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) :
    theorem conjugate_lt_conjugate {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} {b : R} (hab : a < b) {c : R} (hc : IsRegular c) :
    star c * a * c < star c * b * c
    theorem conjugate_lt_conjugate' {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} {b : R} (hab : a < b) {c : R} (hc : IsRegular c) :
    c * a * star c < c * b * star c
    theorem conjugate_pos {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) :
    0 < star c * a * c
    theorem conjugate_pos' {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) :
    0 < c * a * star c
    theorem star_mul_self_pos {R : Type u} [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} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Nontrivial R] {x : R} (hx : IsRegular x) :
    0 < x * star x
    Equations
    • =
    @[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 StarModule.smul_lt_smul_of_pos {R : Type u} {A : Type u_1} [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [StarModule R A] [NoZeroSMulDivisors R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} {b : A} {c : R} (hab : a < b) (hc : 0 < c) :
    c a < c b
    theorem NonUnitalStarRingHom.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) {x : R} {y : R} (hxy : x y) :
    f x f y
    @[instance 100]
    Equations
    • =
    @[instance 100]
    Equations
    • =