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
    Equations
    @[reducible]
    def 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.

    Equations
    Instances For
      @[reducible]
      def 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.

      Equations
      Instances For
        @[reducible]
        def 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.

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