Documentation

Mathlib.Algebra.Order.Star.Basic

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)

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} :
    ∀ {inst : NonUnitalSemiring R} {inst_1 : PartialOrder R} {inst_2 : StarRing R} [self : StarOrderedRing R] (x 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 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_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 IsSelfAdjoint.conjugate_nonneg {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 a) {c : R} (hc : IsSelfAdjoint c) :
    0 c * a * c
    theorem conjugate_nonneg_of_nonneg {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 a) {c : R} (hc : 0 c) :
    0 c * a * 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
    theorem IsSelfAdjoint.conjugate_le_conjugate {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} {b : R} (hab : a b) {c : R} (hc : IsSelfAdjoint c) :
    c * a * c c * b * c
    theorem conjugate_le_conjugate_of_nonneg {R : Type u} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} {b : R} (hab : a b) {c : R} (hc : 0 c) :
    c * a * c c * b * 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 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
    • =