Making Complex generic

Stream: mathlib4

[Adam Nemecek]

Hello,
currently Complex is defined as Complex over R (https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Complex/Basic.lean#L28)
What are people's thought on making Complex generic? Either introduce a new type or making the current type generic. Currently, Complex is a pain to work with if you want to do computation, since e.g. Complex division is noncomputable. Having a computable Complex seems like a good idea.

[Jireh Loreaux]

What do you mean by "have a computable Complex"? Doing you mean you want computable Gaussian integers or something?

[Adam Nemecek]

complex type where all operations are computable. e.g. this

import Mathlib.Data.Complex.Basic
def c1: ℂ := ⟨1.0, 1.0⟩
#eval c1 / c1

fails with "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Complex.instDivInvMonoid', which is 'noncomputable'"

[Adam Nemecek]

this is because R/R is not computable

[Jireh Loreaux]

I'm not sure how you expect division of complex numbers (or real numbers) to be computable.

[Adam Nemecek]

I am not. Which is why I suggest that there is a generic Complex number that can be defined over something where division is computable

[Jireh Loreaux]

Right, but what kinds of things do you want to allow?

[Adam Nemecek]

computable division of Complex over number classes that allow for it

[Jireh Loreaux]

Right, so you want things like Guassian integers. Perhaps then you'll find the discussion here relevant: #mathlib reviewers > Quadratic extensions

[Eric Wieser]

docs#GaussianInt already exists

[Adam Nemecek]

right now, how do i complex over Q?

[Eric Wieser]

You wait for the work in that other thread

[Jireh Loreaux]

oops, that's a private stream :face_palm:

[Adam Nemecek]

i dont have access to view it

[Eric Wieser]

#27511 is probably just as useful

[Jireh Loreaux]

and here is the associated Zulip discussion: #Is there code for X? > Z[(1+sqrt(1+4k))/2] @ 💬

[Kevin Buzzard]

@Yaël Dillies this is another argument for the computable two-field structure rather than your proposal to make noncomputable quadratic algebras.

[Adam Nemecek]

@Kevin Buzzard i think that my argument is for having a generic two-field structure which is computable or not based on the particular type argument

[Kevin Buzzard]

but isn't that the same as "the two-field structure is a computable construction" i.e. "the resulting object is as computable as the input"?

[Artie Khovanov]

@Adam Nemecek Currently you do this by using AdjoinRoot (X ^ 2 + 1 : Polynomial R). But indeed there is a PR for this idea that makes stuff computable, as I understand: https://github.com/leanprover-community/mathlib4/pull/27511

[Niels Voss]

At the very least, I think Complex should refer to the concrete type of complex numbers, and if we want to make a generic version we should give it a different name.

[Mr Proof]

Having tried Lean last year, I was for fun trying to create my own Type Theory language.

Learning from the lessons and mistakes from MathLib, I made sure to make my Complex type be dependent on another number type. e.g. So it would be (complex numbers over integers):

$$\mathbb{C}[\mathbb{Z}]$$

or (complex numbers over reals)

$$\mathbb{C}[\mathbb{R}]$$

or even (complexified complex numbers)

$$\mathbb{C}[\mathbb{C}[\mathbb{Q}]]$$

But, then what I realised was that this was a bit verbose. And that as well as the generic complex type, it was convenient also to have a shorthand for writing the "usual" Complex with two real components just written as

$$\mathbb{C} = \mathbb{C}[\mathbb{R}]$$

But then there is also another one which we often want to make things simpler, complex plane + point at infinity = Riemann sphere

$$\mathbb{C} \cup \{\infty\}$$

So which one to define as "the" complex numbers is up for debate.

Another thing I tried was to not define Complex as a axiomatic type at all but define it as something like Complex := AlgebraicClosure( MetricCompletion( Q )). But that is even more verbose!

[Niels Voss]

Can you explain what you mean by "lessons and mistakes from MathLib"? And do you have a link to your definition of the dependent Complex type?

[Mr Proof]

Niels Voss said:

Can you explain what you mean by "lessons and mistakes from MathLib"? And do you have a link to your definition of the dependent Complex type?

Well, like the OP says, making Complex not a dependent type but making Quaternions dependent on a type e.g. you can do

$$\mathbb{H}[\mathbb{Q}]$$

But Complex seems to assume the parts are real.
Maybe not a mistake but, an asymmetric design choice.

And then having Gaussian integers as a separate type. Not a choice I would have made. But I respect everyone's choices.

*Apologies for my non-standard notation. [..] is meant to mean "over the"

[Niels Voss]

You said you already developed a custom type theory where you made the complex type generic. Where can we find this development?

[Michael Rothgang]

tangential point: I don't see how the Riemann sphere is related to your "complex numbers over another type"

[Mr Proof]

Niels Voss said:

You said you already developed a custom type theory where you made the complex type generic. Where can we find this development?

Well, I said I "tried" to create my own dependent Type Theory language. I didn't say I succeeded very well! :laughing: But you can see my attempt here. And the complex page here.

It is all in Javascript. I just made it because it helped me understand some of the basics of dependent type theory. And it gives me an appreciation of how difficult it is to get right.

Plus I just wanted to see if I could format things in Latex.

@Michael Rothgang (Yeah I was just a side point, about when we talk about Complex numbers sometimes we might include the point at infinity - probably not -, and whether that should be the default setting or not. It's a similar argument to whether natural numbers should include zero. It just a matter of convention. Sorry, it was just an irrelevant tangent. :pensive: )

[Michael Rothgang]

I see. Though I would argue the situation about the natural numbers is different --- $\mathbb{N}_0$ has better algebraic properties than $\mathbb{N}_1$ (it gains a neutral element). You cannot extend addition and multiplication to the Riemann sphere to make it a field. Don't get me wrong, I like the Riemann sphere, but I think the difference is far larger.
In any case, if we want to further discuss this, we should take it elsewhere!

[Eric Wieser]

docs#QuadraticAlgebra has now landed in mathlib!