## Stream: general

### Topic: Poll: partial order on complex numbers in mathlib

/poll

#### Bryan Gin-ge Chen (Feb 11 2021 at 06:18):

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

#### Notification Bot (Feb 11 2021 at 06:20):

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

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


#### 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?

#### 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

#### 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

#### 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"

#### Scott Morrison (Feb 11 2021 at 07:18):

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

#### 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

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

#### Mario Carneiro (Feb 11 2021 at 07:19):

is there a wiki link for this?

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

#### Scott Morrison (Feb 11 2021 at 07:20):

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

#### Scott Morrison (Feb 11 2021 at 07:22):

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

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

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

#### Mario Carneiro (Feb 11 2021 at 07:26):

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

#### 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

#### Mario Carneiro (Feb 11 2021 at 07:31):

or maybe nat subtraction is a better parallel

#### Scott Morrison (Feb 11 2021 at 08:09):

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

#### 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

#### Scott Morrison (Feb 11 2021 at 08:49):

Ok! How should I hide it away?

#### 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

Done!

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

#### Johan Commelin (Feb 24 2021 at 06:37):

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

#### Johan Commelin (Feb 24 2021 at 06:37):

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

#### 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

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

#### 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

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

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

#### Johan Commelin (Feb 24 2021 at 07:52):

ooh, ok :thumbs_up:

#### Gabriel Ebner (Feb 24 2021 at 08:24):

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

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

#### 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 ℂ.

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

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

#### 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


(deleted)

#### 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

#### 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?

#### Damiano Testa (Feb 24 2021 at 08:44):

I was trying to exploit

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


#### Damiano Testa (Feb 24 2021 at 08:44):

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

#### 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?

yes

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

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

#### Mario Carneiro (Feb 24 2021 at 08:48):

which has the advantage of being total

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

#### Mario Carneiro (Feb 24 2021 at 08:50):

It coincides with both

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

#### Damiano Testa (Feb 24 2021 at 08:51):

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

#### 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

#### 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

#### 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