Poll: partial order on complex numbers in mathlib

Stream: general

[Bryan Gin-ge Chen]

/poll

[Bryan Gin-ge Chen]

Oh, would it be better to put the poll in #general?

[Notification Bot]

This topic was moved here from #PR reviews > #4684 by Bryan Gin-ge Chen

[Bryan Gin-ge Chen]

Quoting from #4684:

/--
We put a partial order on ℂ so that `z ≤ w` exactly if `w - z` is real and nonnegative.
Complex numbers with different imaginary parts are incomparable.
-/
instance : partial_order ℂ :=
{ le := λ z w, ∃ x : ℝ, 0 ≤ x ∧ w = z + x,
...

[Johan Commelin]

Are there any other candidates for which we might want to use results from the order library?

[Damiano Testa]

I am not sure whether this is relevant or not, but there are partial orderings on ℂ, different than the one above that appear in the literature. For instance, when talking about Bridgeland stability conditions, (partially) ordering complex numbers by a choice of argument appears often. One example, is on page 2 of the paper below, with even an explanatory picture:

https://www.maths.ed.ac.uk/~abayer/dc-lecture-notes.pdf

[Mario Carneiro]

Well it's not just a matter of whether there is any better order to put on the complexes. Not putting an order on the complexes should also be an option. Sometimes I think that we're undermining the benefits of type theory when we make everything apply to everything like this; I'm reminded of the incident where nat had a has_coe_fn to nat -> nat

[Mario Carneiro]

My rationale is that if you ask a mathematician "are the complexes ordered" the answer you will get is "no"

[Scott Morrison]

I guess my ancient functional analysis origins are showing. I would have said "yes". :-)

[Mario Carneiro]

I have seen this particular order before, I think in coq or mizar, but it seems more like a formalization trick than anything else

[Scott Morrison]

It's the standard ordering on any Banach *-algebra or C*-algebra, specialised to the smallest example of such.

[Mario Carneiro]

is there a wiki link for this?

[Damiano Testa]

Just to clarify: what I meant by my comment is that I personally would not consider the complex numbers to be ordered, but I am happy with someone saying "for this section, I am going to order the complex numbers as follows: [...]". Whether they use the "lexicographic-like" stuff with the reals, arguments, norms, or whatever else is less relevant (to me!).

So, from this point of view, I believe that my position is close to Mario's.

[Scott Morrison]

wikipedia does indeed say the ordering is only on the self-adjoint elements

[Scott Morrison]

https://en.wikipedia.org/wiki/C*-algebra#Structure_of_C*-algebras

[Scott Morrison]

Okay, I'll agree that extending the partial order, rather than just the self-adjoint elements, is not particularly important or useful.

[Scott Morrison]

It's useful for the sake of formalisation, because you don't need to carry around witnesses of self-adjointness when talking about the ordering of self-adjoint elements.

[Mario Carneiro]

well that should be some kind of subspace. Of course this is pretty explicit for real

[Mario Carneiro]

That said I'm sympathetic to the formalization argument and I won't fight too hard on this. I just want to double check that this isn't another division by zero kind of thing that will require us to defend the choice to aghast mainstream mathematicians all the time

[Mario Carneiro]

or maybe nat subtraction is a better parallel

[Scott Morrison]

I'm pretty sure this is no where near as aghasting as monus.

[Kevin Buzzard]

Are we talking about making this a global instance? I think most mathematicians expect C not to have an order

[Scott Morrison]

Ok! How should I hide it away?

[Mario Carneiro]

Like Bryan said, another option is to have this be an instance in a locale. That means you would say open_locale complex_order or something like that and it would add local attribute [instance] complex.partial_order and so on

[Scott Morrison]

Done!

[Scott Morrison]

Reviving this question briefly: someone pointed out to me recently that it is completely standard to write 0 ≤ z in informal mathematics, when z is a complex number to mean "z is real and non-negative".

When the partial_order ℂ discussed above is available, it is possible to do exactly this in Lean too.

[Johan Commelin]

@Scott Morrison do you have particular reasons against using a locale?

[Johan Commelin]

Doesn't that give us the best of both worlds?

[Mario Carneiro]

It's also possible to write I <= z with that partial order, and I'm not sure what this actually means would be in the top 3 guesses if you showed this to a random mathematician

[Mario Carneiro]

(that said, we are of course no strangers to definitions that make sense in a limited range and give pseudo-sensible results out of range)

[Johan Commelin]

Right, we should just define I <= z to mean z = 37 whenever z is non-real :stuck_out_tongue_wink: /s

[Scott Morrison]

It's even pretty sensible: I <= z means z-I is a positive complex number, ie a positive real.

[Scott Morrison]

I don't have my heart set on making this instance global. I just wanted to say that I'd realised people use it naturally.

[Johan Commelin]

ooh, ok :thumbs_up:

[Gabriel Ebner]

Ah great, then we can finally write x ≤ 0 ∨ 0 ≤ x instead of im x = 0.

[Gabriel Ebner]

I would advise against making local(ized) instances for notation classes. This might get confusing because the pretty-printer will always print it as x ≤ 0, but Lean can't parse x ≤ 0 unless the locale is opened.

[Gabriel Ebner]

In a similar vein, I think it would be just as confusing if we had multiple instances for has_le ℂ.

[Gabriel Ebner]

I am not convinced that this type class is a good idea. But if we have it, I think it should be global.

[Gabriel Ebner]

In Scott's example you could just say (z : ℝ) (h : 0 ≤ z) or even (z : ℝ≥0) instead of (z : ℂ) (h : 0 ≤ z) and then use coercions. And the coercion allows simp lemmas to trigger, while the hypothesis doesn't (as easily).

[Damiano Testa]

Following up on Gabriel's comment, the Riemann hypothesis becomes a statement about zeros of the ζ-function lying on the line

{ s : ℂ | I * s ≤ I * 1 / 2 ∨ I * 1 / 2 ≤ I * s }

i.e.

ζ (s) = 0 → I * s ≤ I * 1 / 2 ∨ I * 1 / 2 ≤ I * s

[Gabriel Ebner]

(deleted)

[Damiano Testa]

I could be wrong: I had to change it a few times to get my head around the right condition... ahahah

[Gabriel Ebner]

Second try (this ≤ is really hard to interpret): is this a very convoluted way of saying re s = 1/2?

[Damiano Testa]

I was trying to exploit

x ≤ s ∨ s ≤ x ↔ im x = im s

[Damiano Testa]

Gabriel, indeed, that is what I was trying to achieve! Ahaha

[Damiano Testa]

I view this partial order as uncountably many incomparable orders, one for each imaginary part. On a given line with a fixed imaginary part, you simply compare the real parts. This is what it is, right?

[Mario Carneiro]

yes

[Damiano Testa]

To be honest, I am not thrilled about this order, but I am also unlikely to actually ever seriously use an order on ℂ, so I am happy to go with whatever makes formalizing simpler.

[Mario Carneiro]

There is another order on the complexes that I have used before, namely lexicographic order of (re z, im z)

[Mario Carneiro]

which has the advantage of being total

[Damiano Testa]

The one in question is closer to lex on (im z, re z), except that the order on im is inexistent: you can only compare something with itself.

[Mario Carneiro]

It coincides with both

[Mario Carneiro]

The given partial order is a subset of both total orders (re z, im z) and (im z, re z)

[Damiano Testa]

Yes, you are right: this is so confusing for me! :upside_down:

[Mario Carneiro]

Personally it makes more sense to me to sort the numbers -1, -I, 0, I, 1 in that order

[Mario Carneiro]

like if I had a whole random collection of complex numbers and wanted to arrange them lex order seems the easiest to follow

[Damiano Testa]

My tutees just taught me the "jungle river metric" on ℝ^2, which has similar features (although it does allow you to change the x coordinate, but at a cost).
(You should view the x-axis as a river and you can only travel vertically or along the river, so to go from (a,b) to (c,d) you first go vertically to the x-axis, then you slide on the river and finally you move vertically again)

[Jireh Loreaux]

(Note: what follows was merged from another thread)

With #6210 (see also this thread), the IsROrC class will now extend PartialOrder, so that we can have a StarOrderedRing instance for IsROrC. However, this would entail making the existing scoped PartialOrder ℂ instance a global instance (x ≤ y ↔ x.re ≤ y.re ∧ x.im = y.im). The question is: is that okay?

[Jireh Loreaux]

/poll Can we make the PartialOrder ℂ instance global?
yes
no

[Kalle Kytölä]

What would be the arguments against making this instance global?

Of course, one shouldn't use $\le$ on $\mathbb{C}$ too much in the first place... But when it is used in math, I think it is almost always in exactly the sense (x ≤ y ↔ x.re ≤ y.re ∧ x.im = y.im) that Jireh describes.

Trying to force myself to think of some other mathematically reasonable meaning and use of $\le$ on $\mathbb{C}$, I could only come up with "two-dimensional cumulative distribution functions determining a Borel (probability) measure on $\mathbb{C}$", in which case the reasonable choice of partial order would be (x ≤ y ↔ x.re ≤ y.re ∧ x.im ≤ y.im). But I doubt this other partial order should be a global instance. (For that purpose we have Fin 2 → ℝ, I guess.)

[Jireh Loreaux]

Kalle, turning your comments into an argument against it would go something like this:

"there are other partial orders we may want to consider on ℂ from time to time; e.g., two-dimensional cumulative distribution functions determining a Borel (probability) measure on ℂ result in the pointwise order (x.re ≤ y.re ∧ x.im ≤ y.im). If the instance suggested by the poll is made global, then to use this alternative partial order we would have to disable it locally."

I'm not saying I support that argument, but you asked for an argument against it.

[Eric Wieser]

What would be the arguments against making this instance global?

That the order is surprising for people who aren't paying attention, I guess. Perhaps you wrote z < w but meant to write norm z < norm w or z.re < w.re.
If you think the complex partial order is stupid, then you will be annoyed that this silently did the wrong thing instead of giving you an error.

[Jireh Loreaux]

Eric, I think what you're suggesting is probably (IMHO) the best argument against it. Although I think where it might be most confusing is if you wanted norm z < norm w (or something related), but for some reason they were coerced to ℂ; then Lean doesn't complain, but you didn't get what you expected and it is sometimes easy to miss a ↑ in the goal.

[Eric Wieser]

A good example of another family of scoped instances is the one that sets {1} + {2, 3} = {3, 4}; that's disabled behind the Pointwise locale, even though its the "obvious" instance

[Kevin Buzzard]

I totally agree that the partial order is completely stupid, and indeed am savage with undergraduates when they write $z\leq w$ for complex numbers, but what I am unclear about is whether this instinct is a reasonable basis for arguing against not making the instance global. 6 years ago I would have also argued that $1/0=0$ is also completely stupid and I have now made my peace with this idea having better understood the nature of Lean's type theory.

[Jireh Loreaux]

Kevin, do you think a partial order instance on H →L[ℂ] H with H a Hilbert space is also stupid? (the order is propositionally the same as f₁ ≤ f₂ iff f₂ - f₁ is positive semidefinite.)

[Kevin Buzzard]

A more mathematical comment: a few months ago when thinking about this order I wanted to dismiss it out of hand because everyone knows that (a) there's a standard proof which shows that there's no sensible order on the complexes ("squares are nonnegative and -1 is negative") and hence (b) the complexes are a field and a ring, and this order will not make them an ordered field or an ordered ring, and thus it's a terrible idea. However the argument for (a) shows that there is no total order on the complexes which is compatible with the ring structure (squares are nonnegative because you check the two cases x>=0 and x<0, so the argument doesn't apply to $i$ which is neither > 0 nor < 0) and (b) when I actually started to think about it, the axioms you come up with are satisfied anyway; for example $a\leq b$ and $c\leq d$ doesn't imply $ac\leq bd$, but this isn't true for the reals either; you have to demand $0\leq a$ and $0\leq c$ to make this work, and this is true for the complexes with the proposed order. So even though my gut feeling is that this is horrible, I cannot mathematically justify this and so I might just be wrong.

[Kevin Buzzard]

Jireh I have never seen that ordering in my life but perhaps my answer is: if it is a partial order which satisfies $0\leq 1$, and if $a\leq b$ and $c\leq d$ implies $a+c\leq b+d$, and if it also satisfies $ac\leq bd$ under the additional assumptions $0\leq a$ and $0\leq c$ then I cannot really find a mathematical objection to it.

[Jireh Loreaux]

Kevin, it's the standard order on selfadjoint elements, but extended to be defined on all elements by requiring that the imaginary parts are equal. It definitely doesn't satisfy a * c ≤ b * d if 0 ≤ a and 0 ≤ c because it lacks commutativity (this is partly why a StarOrderedRing is in general not an OrderedRing).

[Kevin Buzzard]

$ac\leq bc\leq bd$?

[Jireh Loreaux]

both of those inequalities fail

[Kevin Buzzard]

Oh interesting. Just to be clear we're assuming $0\leq a$ here, which implies that the imaginary part of $a$ is zero. This doesn't help? This is what saves us in the complexes.

[Jireh Loreaux]

Right, but ℂ is commutative. The product of positive operators is positive if and only if they commute. (Essentially because that's what's needed to make the product selfadjoint)

[Kalle Kytölä]

Thanks everyone for much better arguments than I had in mind!

After these, I do like Eric's balanced vote for both yes and no :rofl:, but I think the self-adjoint use case is so dear to me that I vote for whatever makes it the most convenient (which I believe is Jireh's proposed instance).

[Eric Wieser]

Note that this has been discussed (at least once) before:

Johan Commelin said:

I think it was/is controversial to make that order an instance on ℂ, because it is pretty non-canonical.

[Eric Wieser]

In fact, we even had a poll! (in a different thread again)

[Jireh Loreaux]

Kevin the inequality that holds in a StarOrderedRing is docs#conjugate_le_conjugate a ≤ b → star c * a * c ≤ star c * b * c. (with our definition, this holds for all a b c, but mathematically you should think of a b as being self-adjoint and c as being anything). When your ring is commutative and positive elements (things of the form star c * c) have positive square roots, then you can get 0 ≤ c → a ≤ b → c * a ≤ c * b because sqrt c exists (and is positive, hence selfadjoint too) and c * a = sqrt c * a * sqrt c ≤ sqrt c * b * sqrt b = c * b.

[Anatole Dedecker]

As I said in another thread, the thing that really sold this order to me is the fact that it’s the natural order coming from the star algebra structure.

[Kalle Kytölä]

I see I even upvoted Kevin's message against the instance in that thread, but I think that message gave the impression of using a ≤ b as an obscure form of hypothesis, which I don't think it would be in clear enough operator-theory context.

(But I'm slightly torn: the "readable to any mathematician not familiar with mathlib" is a strong argument, and Eric's position seems ever more tempting. :balance: )

[Anatole Dedecker]

By the way, maybe I’ve been influenced by Lean too early, but I don’t remember ever seeing the order on operators being restricted to self adjoint elements 🤔

[Jireh Loreaux]

As far as readability is concerned, I'm skeptical that this will really be a problem, even in the context of Kevin's message. For example, I think it's totally natural for a mathematician to say that z : ℂ is positive (they mean z ∈ Set.range ((↑) : ℝ≥0 → ℂ)), which is just phrased as 0 ≤ z with this partial order instance. Likewise, to say z : ℂ is not positive just means z ∉ Set.range ((↑) : ℝ≥0 → ℂ) (or ¬ (0 ≤ z).

The only small footgun I see in that regard is that ¬ (0 ≤ z) is not equivalent to z < 0, but of course that's to be expected since ℂ isn't a linear order.

[Eric Wieser]

Eric Wieser said:

In fact, we even had a poll! (in a different thread again)

should we merge these threads? They ask exactly the same question.

[Jireh Loreaux]

@Kevin Buzzard in case it affects your decision, we do already have the StrictOrderedCommRing ℂ instance in the scope in which PartialOrder ℂ is declared.

[Notification Bot]

26 messages were moved here from #general > global PartialOrder ℂ instance by Eric Wieser.

[Kevin Buzzard]

I don't really use the complexes so I was not going to vote.

[Kevin Buzzard]

I mean, I know I made the PR which introduced them to mathlib in 2017 ;-) :older_man: but I've moved on since then :-)

[Kalle Kytölä]

The readability argument is very good against results stated directly about $\mathbb{C}$ using $\le$. But I think the intention is to only put results in the library about generic star-ordered rings (or similar), in which case I don't think we would be actively misleading the mathematician not familiar with mathlib.

(Or maybe the form $0 \le z$ where $z \in \mathbb{C}$ would still be acceptable as a hypothesis, but I think this is still non-misleading.)

[Jireh Loreaux]

Kalle, I'm not sure I agree that we would only have results in the library about generic star ordered rings. I could certainly imagine stating inequalities about continuous functions taking values in ℂ, because these would be relevant to the continuous functional calculus.

[Eric Wieser]

Maybe @Yaël Dillies can give an opinion on whether open scoped Pointwise causes any trouble in combinatorics

[Kalle Kytölä]

Ok, thanks for the warning, Jireh! I think I'm still mildly in favor...

(I think if this weren't a global instance, the files containing those $\mathbb{C}$-specific of $\mathbb{C}$-valued-function-specific results would still make it an instance, and it's not that much of a readability improvement. Ultimately one just has to know the definitions...)

[Eric Wieser]

Ultimately I think the only things to worry about here are:

• People who are confused when they get this partial order and would prefer not to get one
• People who are confused when they expected this order but don't get it (because they forgot to write open scoped ComplexOrder)
• Problems with using open scoped for instances in general

[Damiano Testa]

Would it be possible to pretty-print the order with a subscript as in $\le _{\mathbb{C}}$? My biggest concern is the "surprise" effect of having an order on $\mathbb{C}$.

[Yury G. Kudryashov]

Damiano Testa said:

Would it be possible to pretty-print the order with a subscript as in $\le _{\mathbb{C}}$? My biggest concern is the "surprise" effect of having an order on $\mathbb{C}$.

I hope, someone can write an unexpander for this.

[Yury G. Kudryashov]

Kalle Kytölä said:

The readability argument is very good against results stated directly about $\mathbb{C}$ using $\le$. But I think the intention is to only put results in the library about generic star-ordered rings (or similar), in which case I don't think we would be actively misleading the mathematician not familiar with mathlib.

(Or maybe the form $0 \le z$ where $z \in \mathbb{C}$ would still be acceptable as a hypothesis, but I think this is still non-misleading.)

IMHO, at least comparison with zero should be allowed. Then theorems like docs#Complex.continuousAt_arg can be formulated in a more natural way h : ¬z ≤ 0

[Yaël Dillies]

Eric Wieser said:

Maybe Yaël Dillies can give an opinion on whether open scoped Pointwise causes any trouble in combinatorics

Absolutely not. pointwise is in fact my most frequently opened locale.

[Eric Wieser]

@Sebastien Gouezel, @Oliver Nash, @Anne Baanen, @Floris van Doorn: has your opinion changed in the two years between the polls?

[Anne Baanen]

If I understand the message history here correctly: the plan is to make docs#StarOrderedRing a superclass of docs#IsROrC, which would make the currently scoped order on ℂ a global instance?

[Anne Baanen]

My hesitation to make the order global is that it wasn't obviously the right one and we might want other orders instead. StarOrderedRing sounds appropriately general so in that case I'm happy with the change.

[Eric Wieser]

That's not really what this poll is about though: we can make the superclass without making it global, so we don't need to mix the votes here

[Eric Wieser]

Unless your comment is "oh, this is obviously the right order after all!"

[Anne Baanen]

I see, then I suppose I have one more question: did anyone need to put another order on ℂ in the meantime?

[Eric Wieser]

I think the answer to that is probably no.

[Anne Baanen]

Alright, thanks for catching me up! Then my vote is now weak support for scoped.

[Oliver Nash]

Eric Wieser said:

Oliver Nash: has your opinion changed in the two years between the polls?

No, but I haven't thought carefully about this so I decided not to vote in the new poll.

[Oliver Nash]

Eric Wieser said:

we can make the superclass without making it global, so we don't need to mix the votes here

Looking quickly now I cannot easily reconcile this claim witht he claim in new poll saying that we would have to make the partial order instance global to create the star-ordered ring instance.

[Oliver Nash]

To be totally honest, I think there are already enough oars in this boat so I'm reluctant to spend time on it.

[Yury G. Kudryashov]

We can add le and lt fields to IsROrC instead of adding PartialOrder K to extends.

[Yury G. Kudryashov]

But I would prefer to have a global StarOrderedRing instance.

[Floris van Doorn]

Given that we now have a StarOrderedRing class for which the complexes are an instance, I don't feel strongly anymore about my position to keep the order on ℂ scoped. I think we can still keep it scoped (it seems to work fine for the pointwise operations on sets - so I see no reason it would be annoying here), but it's also ok with me if we make it global.