Zulip Chat Archive

Stream: maths

Topic: Ideal class group


view this post on Zulip Anne Baanen (May 18 2020 at 09:13):

I'd like to talk about the class group of a number field, so I want to get started on the number fields project. @Filippo A. E. Nuccio, you were considering Dedekind rings last week, how much did you (plan to) do, so we don't overlap our efforts?

(Background: I've been doing some work on quadratic forms and this is a good way to turn it into more "fashionable" mathematics.)

view this post on Zulip Kevin Buzzard (May 18 2020 at 09:14):

I think quadratic forms are perfectly fashionable! There are links to Galois cohomology too:-)

view this post on Zulip Anne Baanen (May 18 2020 at 09:24):

Apologies. The correct phrasing was "fashionable mathematics that I know enough about to formalise in Lean" :)

view this post on Zulip Johan Commelin (May 18 2020 at 09:27):

Note that I created a project on github for tracking the classification of QF's over Q a while ago.

view this post on Zulip Johan Commelin (May 18 2020 at 09:28):

It's related but unrelated (-;

view this post on Zulip Alex J. Best (May 18 2020 at 09:51):

I remember a long time ago we talked about number fields and Kevin mentioned some imperial students had some work on it? But maybe at this point its better to just start something fresh seeing as mathlib has progressed a lot.

view this post on Zulip Kevin Buzzard (May 18 2020 at 09:54):

I am not sure anything survived from Imperial. I think a lot of people have made half-starts on Dedekind domains but the big peak (a definition of Dedekind domain which makes it possible both to prove that the integers of a number field are a Dedekind domain, and that every non-zero ideal in a Dedekind domain is uniquely a product of prime ideals) remains unconquered. The definition of the peak is slightly convoluted because there are several definitions of Dedekind Domain in Cassels-Froehlich, one of which is "an integral domain where every non-zero ideal factors uniquely into a product of prime ideals"! One has to ensure that one has enough to relate it back to number fields.

view this post on Zulip Alex J. Best (May 18 2020 at 09:58):

Right, given Anne's work on fractional ideals I guess we can now give definition DD3 from https://en.wikipedia.org/wiki/Dedekind_domain using just mathlib stuff. We don't have Krull dimension right?

view this post on Zulip Alex J. Best (May 18 2020 at 10:04):

As for finiteness of the class group and dirichlet, are there any nices way to do them without Minkowski's theorem? Not that I don't like Minkowski, but it seems a lot of theory to set up to me.

view this post on Zulip Kevin Buzzard (May 18 2020 at 10:06):

There is a general statement about compactness of the norm 1 elements of the idele class group proved in Cassels' article, which I have always thought of as somehow equivalence to both finiteness of the ideal class group and the assertion that the rank of the unit group is what it is. I am unfortunately busy with something else right now so cannot chase up. @Johan Commelin do you know anything about this?

view this post on Zulip Alex J. Best (May 18 2020 at 10:12):

https://mathoverflow.net/questions/19021/avoiding-minkowskis-theorem-in-algebraic-number-theory points to Ireland-Rosen which looks pretty good to me, instead of making an argument involving volume they partition the unit cube into a bunch of subcubes and use the pidgeonhole principle on these subcubes. So it's a weaker bound but seems more easily formalizable (to me).

view this post on Zulip Johan Commelin (May 18 2020 at 10:58):

Kevin Buzzard said:

There is a general statement about compactness of the norm 1 elements of the idele class group proved in Cassels' article, which I have always thought of as somehow equivalence to both finiteness of the ideal class group and the assertion that the rank of the unit group is what it is. I am unfortunately busy with something else right now so cannot chase up. Johan Commelin do you know anything about this?

No, unfortunately I don't know enough details here.

view this post on Zulip Johan Commelin (May 18 2020 at 10:58):

Alex J. Best said:

https://mathoverflow.net/questions/19021/avoiding-minkowskis-theorem-in-algebraic-number-theory points to Ireland-Rosen which looks pretty good to me, instead of making an argument involving volume they partition the unit cube into a bunch of subcubes and use the pidgeonhole principle on these subcubes. So it's a weaker bound but seems more easily formalizable (to me).

That's interesting!

view this post on Zulip Anne Baanen (May 18 2020 at 10:58):

Alex J. Best said:

We don't have Krull dimension right?

I can't find anything related to "Krull" in mathlib, or "dim" in algebra-related subdirectories, so I believe not.

view this post on Zulip Johan Commelin (May 18 2020 at 10:59):

Otoh, Minkowski could be done almost orthogonally, and we have stuff about convex sets etc... already.

view this post on Zulip Patrick Massot (May 18 2020 at 10:59):

I was taught how to prove all this only using ideas from Arakelov geometry, this may be a bit extreme.

view this post on Zulip Johan Commelin (May 18 2020 at 10:59):

Dimension theory is another thing that is well in reach, I would say.

view this post on Zulip Johan Commelin (May 18 2020 at 10:59):

@Patrick Massot Wow, that sounds pretty hardcore

view this post on Zulip Patrick Massot (May 18 2020 at 11:00):

This was a course by Christophe Soulé

view this post on Zulip Patrick Massot (May 18 2020 at 11:01):

I think the ideas came from Szpiro, so formalizing this would be timely

view this post on Zulip Anne Baanen (May 18 2020 at 11:12):

Let's say we use condition DD3:

import ring_theory.fractional_ideal

open localization

namespace ring

/-- DD3: all nonzero fractional ideals are invertible -/
def DD3 (R : Type*) [integral_domain R] :=
 {I : fractional_ideal R (non_zero_divisors R)}, I  0  I * I⁻¹ = 1

end ring

To show ℤ satisfies DD3, we shouldn't need too much:

  • a notion of principal fractional ideal (I guess we should define "principal (semi)module" instead of "principal ideal"?)
  • all fractional ideals are principals if(f) all integral ideals are
  • principal fractional ideals are invertible (this is useful for the class group)

view this post on Zulip Johan Commelin (May 18 2020 at 11:21):

Aren't you outlining the proof that works for arbitrary PIDs?

view this post on Zulip Anne Baanen (May 18 2020 at 11:21):

Indeed, but ℤ is a nice test case :-)

view this post on Zulip Filippo A. E. Nuccio (May 18 2020 at 14:12):

@Anne Baanen Hi! Great to hear that you'd like to develop the class group. I am sure that you are much more comfortable than I am with Lean. I haven't done much yet, because I have been advised to go through the complex numbers game and I am still finishing it.

view this post on Zulip Anne Baanen (May 18 2020 at 14:15):

OK! I'll start with the inverses of principal ideals. Whenever you're ready for the Dedekind domains, just let me know and I'll be happy to get you up to speed :)

view this post on Zulip Filippo A. E. Nuccio (May 18 2020 at 14:15):

So, I guess that if you want to lead the project and you want to assign me tasks to perform, I am eager to do so!

view this post on Zulip Filippo A. E. Nuccio (May 18 2020 at 14:16):

Whenever you want to start, I'll be happy (eg.: now)

view this post on Zulip Johan Commelin (May 18 2020 at 15:21):

@Anne Baanen Note that #2714 is making a lot of changes to fractional ideals

view this post on Zulip Johan Commelin (May 18 2020 at 15:21):

It might be helpful to get that PR merged first

view this post on Zulip Johan Commelin (May 18 2020 at 15:21):

Because you'll probably benefit from the new localisation API

view this post on Zulip Anne Baanen (May 18 2020 at 15:24):

The PR's changes were more extensive than I anticipated, so thanks for the notification!

view this post on Zulip Johan Commelin (May 18 2020 at 15:25):

Would you mind reviewing the fractional ideal part?

view this post on Zulip Johan Commelin (May 18 2020 at 15:25):

You know that part the best, and you know which plans you have

view this post on Zulip Anne Baanen (May 18 2020 at 15:26):

Sure, I'll try to look into it after I help Filippo get set up and before I need to cook dinner :)

view this post on Zulip Ashwin Iyengar (May 18 2020 at 19:53):

I started writing up a file for Dedekind domains a few weeks ago, but got sidetracked into working on an interface for discrete valuation rings. I'll hopefully have DVRs in some kind of stable form later this week!

view this post on Zulip Ashwin Iyengar (May 18 2020 at 19:54):

Which may help with the Dedekind domain stuff.

view this post on Zulip Anne Baanen (May 19 2020 at 08:06):

Great!


Last updated: May 06 2021 at 17:38 UTC