Star ordered ring

Stream: maths

[Frédéric Dupuis]

We currently have the typeclass star_ordered_ring that is meant to capture the order structure of star algebras, which generalizes the semidefinite ordering on matrices, i.e. $A ≤ B$ iff $B-A$ is positive semidefinite. However, as it stands, it doesn't do this: [star_ordered_ring R] requires R to be an ordered_semiring, which includes axioms such as ∀ (a b c : α), a < b → 0 < c → c * a < c * b which we definitely don't want. Also, it only requires that 0 ≤ star r * r for every r, and it's not clear to me how to exclude other elements without making it an iff.

My proposal would be the following: redefine star_ordered_ring as:

class star_ordered_ring (R : Type u) [semiring R] [partial_order R] extends star_ring R :=
(add_le_add_left       : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b)
(le_of_add_le_add_left : ∀ a b c : R, a + b ≤ a + c → b ≤ c)
(nonneg_iff            : ∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s)

(The first two axioms are just copied from ordered_cancel_add_comm_monoid.) I would be interested in feedback on this before I actually do it. @Scott Morrison @Jireh Loreaux @Eric Wieser ?

[Kevin Buzzard]

So you're saying a star ordered ring shouldn't be an ordered ring?

[Oliver Nash]

Has ordered_semiring changed since #4685? In the original discussion of star_ordered_ring it looks like Scott double-checked that ℂ was a star_ordered_ring https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bell.20and.20Tsirelson.20inequalities/near/212407651

[Jireh Loreaux]

Some notes:

1. This has the slightly unnatural but perhaps convenient side effect that certain pairs of non-selfadjoint elements are comparable so long as their difference is selfadjoint and positive.
2. I don't see how to exclude non-positive elements without the iff in the typeclass either; however, given a ⋆-ring, couldn't we always just define this order inductively? For example, maybe something like

import algebra.star.basic
universe u
inductive star_le (R : Type u) [semiring R] [star_ring R] : R → R → Prop
| zero_le_star_self : ∀ r : R, star_le 0 (star r * r)
| add_le_add_left : ∀ r s t : R, star_le r s → star_le (t + r) (t + s)

I'm not sure what the advantages / disadvantages of inductive predicates like this may be.

3. There is another different ⋆-order (in this order, 0 is minimal) which can be placed on ⋆-rings, namely the order due to Drazin: https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society-new-series/volume-84/issue-1/Natural-structures-on-semigroups-with-involution/bams/1183540393.full

[Jireh Loreaux]

Kevin Buzzard said:

So you're saying a star ordered ring shouldn't be an ordered ring?

Maybe not? The multiplicative property is the problem as indicated.

[Frédéric Dupuis]

Maybe we should change the name...? I don't really have a better one in mind though.

[Jireh Loreaux]

Oliver Nash said:

Has ordered_semiring changed since #4685? In the original discussion of star_ordered_ring it looks like Scott double-checked that ℂ was a star_ordered_ring

The problem wouldn't show up with ℂ because it's commutative (and maybe also because it has square roots?).

[Frédéric Dupuis]

Oliver Nash said:

Has ordered_semiring changed since #4685? In the original discussion of star_ordered_ring it looks like Scott double-checked that ℂ was a star_ordered_ring https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bell.20and.20Tsirelson.20inequalities/near/212407651

The current definition works in the commutative case, but the problem is that for, say, matrices, if $A$ and $B$ are positive semidefinite, then $AB$ is not necessarily PSD.

[Jireh Loreaux]

Exactly

[Frédéric Dupuis]

Jireh Loreaux said:

I'm not sure what the advantages / disadvantages of inductive predicates like this may be.

The issue with this is that we want to allow the order to come from somewhere else -- for example, ℂ and ℝ already have an order defined on them, and we just want a typeclass that expresses the fact that the preexisting order is compatible with the star structure.

[Frédéric Dupuis]

And I think the fact that two elements are comparable if their difference is nonnegative should be fine. We've had this order on the complex numbers for a while now and it hasn't caused problems.

[Jireh Loreaux]

Yeah, it just surprised me a bit, but it makes sense. It seems like it would actually be quite convenient from time to time.

[Jireh Loreaux]

Does the removal of ∀ (a b c : α), a < b → 0 < c → c * a < c * b break Scott's proof of CHSH?

[Frédéric Dupuis]

Hmm, good question!

[Jireh Loreaux]

Frédéric Dupuis said:

Maybe we should change the name...? I don't really have a better one in mind though.

Note: if we do keep the name, it definitely deserves a prominent (boldface?) mention in the docstring that it does not extend ordered_semiring along with an explanation for the reason why.

[Jireh Loreaux]

Also of note: for the commutative ⋆-rings, like ℝ, ℂ or α →ᵇ β (with appropriate typeclass assumptions), there will be some redundant lemmas coming from the typeclasses star_ordered_ring and ordered_semiring (namely add_le_add_left). I don't think this matters since it isn't data, but I thought I would mention it in case it matters to someone who knows more than me.

[Frédéric Dupuis]

Jireh Loreaux said:

Also of note: for the commutative ⋆-rings, like ℝ, ℂ or α →ᵇ β (with appropriate typeclass assumptions), there will be some redundant lemmas coming from the typeclasses star_ordered_ring and ordered_semiring (namely add_le_add_left). I don't think this matters since it isn't data, but I thought I would mention it in case it matters to someone who knows more than me.

Right, I don't think that really matters either.

[Frédéric Dupuis]

#11213

[Eric Wieser]

Revisiting this over a year later; is nonneg_iff really the standard axiom here? It seems to rule out rat being a docs#star_ordered_ring under the trivial star operation

[Eric Wieser]

The context for my question is #18818, but it can be expressed more simply as "can we prove docs#matrix.dot_product_self_eq_zero as a special case of docs#matrix.dot_product_star_self_eq_zero with star x = x"?

[Eric Wieser]

My suggestion in #18819 is

class star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R]
  extends star_ring R :=
(add_le_add_left       : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b)
(conjugate_nonneg      : ∀ c r : R, 0 ≤ c → 0 ≤ star r * c * r)
(star_mul_self_nonneg  : ∀ r : R, 0 ≤ star r * r)

which i suspect is enough to satisfy all the current uses in mathlib

[Eric Wieser]

I guess @Frédéric Dupuis's TODO comment that says

In a Banach star algebra without a well-defined square root, the natural ordering is given by the
positive cone which is the closure of the sums of elements star r * r. A weaker version of
star_ordered_ring could be defined for this case. Note that the current definition has the
advantage of not requiring a topology.

is probably a better solution, but perhaps my proposal is still a better compromise than the current definition

[Jireh Loreaux]

Changing it to something without an iff (at least something for which the iff isn't provable under some more hypotheses like closedness of the positive elements) will break C-star-algebra theory (in a few months).

It doesn't break C-star-algebra theory yet because I haven't yet proven (in mathlib, I have it locally) that an element of a complete normed c-star ring over the complex numbers is selfadjoint with nonnegative spectrum if and only if it can be written as star x * x for some x. But once I do, it will be absolutely essential for the rest of the theory.

[Eric Wieser]

That certainly sounds like a more compelling argument than mine, thanks!

[Eric Wieser]

Are you arguing against Frédéric's proposed generalization too?

[Jireh Loreaux]

No, because selfadjoint elements with nonnegative spectrum are closed (in the setting mentioned above), and hence with the aforementioned lemma, so are the elements of the form star x * x. So the closure is just this set of elements.

[Jireh Loreaux]

So the generalization is fine.

[Jireh Loreaux]

You could just create a weaker type class if you wanted though.

[Frédéric Dupuis]

Do you think this generalization would be useful? I don't remember the details of the rabbit hole I went down when I wrote this TODO...!

[Eric Wieser]

As an interim generalization, is ∀ x, 0 ≤ x ↔ x ∈ add_submonoid.closure {(s * star s) | (s : R)} sensible?

[Eric Wieser]

I don't really have an intuition for the relevance of the topological closure here, but the additive closure is enough to include ℚ and presumably the gaussian integers

[Frédéric Dupuis]

Seems OK to me.

[Jireh Loreaux]

Hold on, let me think about it.

[Jireh Loreaux]

I just want to make sure it doesn't make something else really hard.

[Eric Wieser]

No rush, I don't desperately need it, and won't try to rush though a refactor

[Jireh Loreaux]

Wait, how does that work for \Q? In particular, how is 2 positive?

[Frédéric Dupuis]

2 = 1+1

[Jireh Loreaux]

I guess for any positive rational p/q, it is the sum of pq copies of 1/q^2, so it works in general.

[Eric Wieser]

I'll admit I claimed that without a proof in mind, thanks for providing one

[Jireh Loreaux]

Okay, so the effect of this change is that it turns the positive elements into an add_submonoid. For C*-algebras this is already true. The effect this has on me is that it forces me to first show this fact before I can use hypotheses of the form 0 \le x effectively. I'm okay with that for the sake of being able to unify some other things.

One last thing: are we sure this won't cause other headaches (like for CHSH)? I can't think of any examples where the positive elements shouldn''t form a submonoid, and it would be weird if they didn't. But if we could think of an example, that would be a problem.

[Reid Barton]

Eric can you explain the motivation for this?

[Reid Barton]

You mention docs#matrix.dot_product_self_eq_zero but, in general, "if a sum of squares is zero then all the elements are zero" is a lot weaker than "every nonnegative element is a sum of squares".

[Reid Barton]

For instance, not every nonnegative polynomial in $\mathbb{R}[X,Y,Z]$ is a sum of squares.

[Reid Barton]

Or a more elementary/maybe more convincing example: take $\mathbb{R}[X]$ with the ordering given by evaluation at large positive $X$

[Jireh Loreaux]

Reid, a more convincing example of what, exactly? I agree with this:
Reid Barton said:

"if a sum of squares is zero then all the elements are zero" is a lot weaker than "every nonnegative element is a sum of squares".

But I'm not sure exactly what point you are trying to make. I wouldn't expect either of your examples to be star_ordered_rings (under any definition close to our current one).

[Reid Barton]

An example where squares are nonnegative (and so if a sum of squares is zero, then each of the things is zero) but where not every positive element is a sum of squares (e.g., $X$).

[Reid Barton]

I also don't understand what point Eric is trying to make; that's my main point.

[Reid Barton]

I'm not really a fan of inventing new "notions" just to "generalize" lemmas--if one really wants to do this then just turn the statement of every lemma into a class, and the proof of the lemma into an instance.

[Reid Barton]

Doing this to docs#matrix.dot_product_self_eq_zero already seems like a better idea than changing star_ordered_ring.

[Reid Barton]

Even an ordered field doesn't have to satisfy "every nonnegative element is a sum of squares".

[Jireh Loreaux]

Per this paper: https://www.ams.org/tran/1953-074-01/S0002-9947-1953-0054175-2/S0002-9947-1953-0054175-2.pdf, I think that Eric's new definition is the correct one, modulo the topological closure. Note, this doesn't mean the lemma in question should necessarily have its hypotheses changed.

[Jireh Loreaux]

Note that taking the definition (as per the paper) of the positive elements to be the topological closure of the additive submonoid generated by elements of the form star x * x would make a linearly ordered field which contains \Q as a dense set into a star_ordered_ring with the trivial star operation.

[Jireh Loreaux]

@Reid Barton do you still have objections? I'm interested in your thoughts on this.

[Jireh Loreaux]

@Eric Wieser for reasons unrelated to the above discussion, I now actively prefer the definition of star_ordered_ring to use: ∀ x, 0 ≤ x ↔ x ∈ add_submonoid.closure {(s * star s) | (s : R)} instead. The short explanation is I want to declare, for star_ordered_rings, the type of positive elements as a an add_submonoid. This is for reasons related to the API I am developing for the continuous functional calculus.

The slightly longer version is that a continuous functional calculus for normal elements (in a topological ℂ-algebra) descends in a natural way to normal elements whose spectra are contained in ℝ (in which case you get something for selfadjoint elements), or in ℝ≥0 (in which case you get something for positive elements). We want to be able to consider the latter as an ℝ≥0-linear map, but first we need the positive elements to have an add_comm_monoid structure.

Pinging @Reid Barton because you seemed to care about this, and @Frédéric Dupuis because we've been having discussions related to this topic privately.

[Jireh Loreaux]

(deleted) wrong thread

[Reid Barton]

All I really wanted to say is that for the purpose of general algebra, if you want to prove $v^T v = 0 \implies v = 0$ say, then assuming that every nonnegative element is a sum of squares is too strong. Because this holds for all ordered fields, say, and for those there's no reason that every nonnegative element should be a sum of squares.

[Reid Barton]

So wanting to make $\mathbb{Q}$ a star_ring in order to prove that fact about it, and adopting the proposed axiom for that specific purpose, doesn't really make sense, since it still excludes many other ordered fields.

[Kevin Buzzard]

I think the way to proceed here is to define the Stufe of a field; a field has infinite Stufe iff $v^tv=0\implies v=0$.

[Kevin Buzzard]

In fact infinite Stufe iff orderable, apparently.

[Jireh Loreaux]

Sure, as I mentioned before, I think the issue with the definition of star_ordered_ring is not related to whether we should refactor that lemma (despite the fact that this was Eric's original motivation). Note though, Reid, that a star_ordered_ring is not an ordered_ring anyway. It's really a different beast. However, I think it makes sense to have ℚ be a star_ordered_ring, apart from refactoring the lemma, and also this will play better for my purposes in C⋆-algebra theory.

[Jireh Loreaux]

@Eric Wieser FYI: I'm working on the refactor now.

[Eric Wieser]

I've not attempted it anyway, but thanks for letting me know not to

[Eric Wieser]

Out of curiosity, are you actively against the extra topological constraints, or are you just agreeing with my claim that in the short term they matter less than the add_submonoid.closure change?

[Jireh Loreaux]

I'm only against the topological constraints insofar as they increase the type class burdens on the definition (and in our examples so far it only serves to complicate things). If we come across a situation where we need the topological closure instead we can re-evaluate, but I suspect it will be rare.

[Jireh Loreaux]

Although there is the annoying fact I find during the refactor that thesubmonoid_closure is not already imported in that file, and adding that import violates some assert_not_exists clauses.

[Scott Morrison]

I would endorse removing an assert_not_exists clause for a refactor like this! :-)

[Eric Wieser]

I think those clauses are more of a canary for reviewers to see and discuss than a hard rule about where the imports should lie.

[Jireh Loreaux]

#18854. I left the assert_not_exists untouched, so it doesn't build right now, but other than that it should. So please let me know how you think these should be changed. I assume we want to replace them with something else.

[Reid Barton]

Is "star ordered ring" an existing concept in the literature?

[Reid Barton]

The situation I know more about is real closed rings. These have a "continuous semialgebraic functional calculus" as you might call it, and in fact we might as well use that as the definition of a real closed ring. If you have such a calculus then you have a partial order ($0 \le x \iff x = |x|$) and then it follows that any nonnegative element is a square (since if $x = |x|$, then $x$ is the square of $\sqrt{|x|}$).

[Reid Barton]

What I'm not sure about is what corresponds to the "star ordered rings" here, and what the role of the axiom about nonnegative elements being a sum of squares should be.

[Reid Barton]

("Ring" in this context means "commutative ring".)

[Jireh Loreaux]

Can you please elaborate on what you mean by continuous semialgebraic functional calculus?

[Frédéric Dupuis]

Star ordered rings are meant to model objects like hermitian matrices with the positive semidefinite order. Things get a bit tricky because it would be nice, for example, to be able to state that a matrix with entries in $\mathbb{Q}$ is positive-semidefinite.

[Reid Barton]

Jireh Loreaux said:

Can you please elaborate on what you mean by continuous semialgebraic functional calculus?

Given a continuous semialgebraic function, you can evaluate it on an element of any real closed ring.

[Reid Barton]

In fact, real closed rings are the algebras for the Lawvere theory of all continuous semialgebraic functions.

[Eric Wieser]

Reid Barton said:

If you have such a calculus then you have a partial order ($0 \le x \iff x = |x|$) and then it follows that any nonnegative element is a square (since if $x = |x|$, then $x$ is the square of $\sqrt{|x|}$).

To make this work for star rings is the rule just $0 \le x \iff x x^* = x^2$? No, obviously not because this doesn't work for $-1 : \mathbb{Q}$

[Reid Barton]

Explicitly, to give a real closed ring is the same as to give a set $A$ together with, for every continuous semialgebraic function $f : \mathbb{\tilde Q}^n \to \mathbb{\tilde Q}$, a corresponding operation $\underline{f} : A^n \to A$, compatible with compositions and projections. If you use the reals $\mathbb{R}$ or another real closed field in place of $\mathbb{\tilde Q}$ then you get real closed $\mathbb{R}$-algebras.
There's a theorem here, that real closed rings (or $\mathbb{R}$-algebras) end up being a full subcategory of all rings (or $\mathbb{R}$-algebras), so there is also some way to identify the real closed rings as the rings with some extra properties.

[Reid Barton]

Every ring R (doesn't have to be ordered!) has a real spectrum Sper R and the ring of functions on this thing is a real closed ring, the real closure of R.

[Reid Barton]

So I think real closed rings are like the real, commutative, algebraic analogue of C* algebras.

[Reid Barton]

And I guess ordinary rings correspond to star rings. But I don't know what should correspond to star ordered rings.

[Reid Barton]

I know there are various notions of ordered ring like poring, f-ordered ring, lattice ordered ring, but I haven't had occasion to use those

[Jireh Loreaux]

Thanks for the explanation.