Quadratic fields

Stream: maths

[Paul van Wamelen]

I'd like to add the ring of quadratic integers for the case when d is 1 mod 4. So the ring of the integers adjoined with (1 + a square root of d)/2. What should these be called? We already have zsqrtd = ℤ√d. I was thinking of using 𝒪√d? What should the file be called? Also, the elements have the form a + b (1 + √d)/2 where a b : ℤ. Should I call a and b, re and im (as in zsqrtd)? I would rather just call them c1 and c2 (for component 1 and 2) especially since the components in the embedding in ℂ isn't the real and imaginary parts. I'd love to hear people's thoughts on this!

[Kevin Buzzard]

This is a very delicate question! Each new definition added to lean comes with a cost so you want to make sure you've got it right the first time. Are you happy to have these rings for d which aren't fundamental discriminants eg 45 or even 9?

[Kevin Buzzard]

Then there's the implementation question of whether you should define it under the hood to be a pair of integers (which Mario might be tempted to do) or as a quotient of Z[X] (which I'd be tempted to do). @Chris Hughes which one is the best idea?

[Kevin Buzzard]

This question doesn't matter to a mathematician because all we want is the interface, but someone has to make it and the job is very different depending on which definition you choose

[Kevin Buzzard]

I should say that your ideas all look fine to me and that you should perhaps allow all integers d in the definition and just make the ring structure for d congruent to 1 mod 4, but actually this then presents a problem for type class inference

[Kevin Buzzard]

Another approach would be to define integers of number fields, which I think we have already, and then define these functions c1 and c2 for the quadratic fields in question.

[Kenny Lau]

I propose defining Z[(1+sqrt(1+4k))/2]

[Kenny Lau]

just to make sure that it's always a ring

[Kenny Lau]

$\left(\frac{1+\sqrt{1+4k}}2\right)^2 = \frac{2+4k+2\sqrt{1+4k}}{4} = k + \frac{1+\sqrt{1+4k}}2$

[Kenny Lau]

you can call it Zhopsopft for "Z half one plus square-root one plus four times"

[Chris Hughes]

There is already zsqrtd. I agree with the simple construction as pairs, it will given some nicer definitional equalities.

[Johan Commelin]

We probably need a name for this gadget... should we have roi2 or quadratic_ring_of_integers that gives the correct thing for all non-square d?

[Paul van Wamelen]

I'm using d1_quadratic_int for now... (I think that is an improvement on Zhopsopft :grinning_face_with_smiling_eyes: )

[Johan Commelin]

@Kevin Buzzard would it make sense to define this to be int x int or int[epsilon] in the cases where Q[X](X^2 - d) is not a field?

[Kevin Buzzard]

Sure. I haven't looked but I bet that's what Mario did with Zsqrtd when d was a square. I was much less sure about how to deal with the d=1 mod 4 thing but maybe Kenny's solution is the best