Zulip Chat Archive

Stream: maths

Topic: Quadratic fields


view this post on Zulip Paul van Wamelen (Sep 04 2020 at 02:20):

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!

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 08:07):

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?

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 08:10):

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?

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 08:11):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 08:13):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 08:17):

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.

view this post on Zulip Kenny Lau (Sep 04 2020 at 08:34):

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

view this post on Zulip Kenny Lau (Sep 04 2020 at 08:34):

just to make sure that it's always a ring

view this post on Zulip Kenny Lau (Sep 04 2020 at 08:59):

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

view this post on Zulip Kenny Lau (Sep 04 2020 at 09:01):

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

view this post on Zulip Chris Hughes (Sep 04 2020 at 09:12):

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

view this post on Zulip Johan Commelin (Sep 05 2020 at 15:36):

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?

view this post on Zulip Paul van Wamelen (Sep 05 2020 at 15:57):

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

view this post on Zulip Johan Commelin (Sep 05 2020 at 16:04):

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

view this post on Zulip Kevin Buzzard (Sep 05 2020 at 16:06):

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


Last updated: May 06 2021 at 17:38 UTC