Zulip Chat Archive

Stream: general

Topic: Poll: partial order on complex numbers in mathlib


view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 06:17):

/poll

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 06:18):

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

view this post on Zulip Notification Bot (Feb 11 2021 at 06:20):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 06:21):

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

view this post on Zulip Johan Commelin (Feb 11 2021 at 06:49):

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

view this post on Zulip Damiano Testa (Feb 11 2021 at 06:58):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:15):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:16):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 07:18):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:18):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 07:18):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:19):

is there a wiki link for this?

view this post on Zulip Damiano Testa (Feb 11 2021 at 07:20):

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.

view this post on Zulip Scott Morrison (Feb 11 2021 at 07:20):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 07:22):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 07:23):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 07:23):

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.

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:26):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:30):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 07:31):

or maybe nat subtraction is a better parallel

view this post on Zulip Scott Morrison (Feb 11 2021 at 08:09):

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

view this post on Zulip Kevin Buzzard (Feb 11 2021 at 08:32):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 08:49):

Ok! How should I hide it away?

view this post on Zulip Mario Carneiro (Feb 11 2021 at 08:51):

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

view this post on Zulip Scott Morrison (Feb 11 2021 at 09:57):

Done!

view this post on Zulip Scott Morrison (Feb 24 2021 at 06:25):

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.

view this post on Zulip Johan Commelin (Feb 24 2021 at 06:37):

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

view this post on Zulip Johan Commelin (Feb 24 2021 at 06:37):

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

view this post on Zulip Mario Carneiro (Feb 24 2021 at 06:52):

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

view this post on Zulip Mario Carneiro (Feb 24 2021 at 06:54):

(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)

view this post on Zulip Johan Commelin (Feb 24 2021 at 06:56):

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

view this post on Zulip Scott Morrison (Feb 24 2021 at 07:41):

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

view this post on Zulip Scott Morrison (Feb 24 2021 at 07:42):

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.

view this post on Zulip Johan Commelin (Feb 24 2021 at 07:52):

ooh, ok :thumbs_up:

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:24):

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

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:26):

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.

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:26):

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

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:28):

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

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:30):

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

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:36):

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

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:42):

(deleted)

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:42):

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

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:43):

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

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:44):

I was trying to exploit

x  s  s  x  im x = im s

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:44):

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

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:46):

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?

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:46):

yes

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:47):

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.

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:48):

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

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:48):

which has the advantage of being total

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:49):

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.

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:50):

It coincides with both

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:50):

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

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:51):

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

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:52):

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

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:53):

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

view this post on Zulip Damiano Testa (Feb 24 2021 at 08:54):

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)


Last updated: May 10 2021 at 18:22 UTC