Stream: maths

Topic: Ideal class group

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

Kevin Buzzard (May 18 2020 at 09:14):

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

Anne Baanen (May 18 2020 at 09:24):

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

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.

Johan Commelin (May 18 2020 at 09:28):

It's related but unrelated (-;

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.

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.

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?

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.

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?

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

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.

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!

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.

Johan Commelin (May 18 2020 at 10:59):

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

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.

Johan Commelin (May 18 2020 at 10:59):

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

Johan Commelin (May 18 2020 at 10:59):

@Patrick Massot Wow, that sounds pretty hardcore

Patrick Massot (May 18 2020 at 11:00):

This was a course by Christophe Soulé

Patrick Massot (May 18 2020 at 11:01):

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

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)

Johan Commelin (May 18 2020 at 11:21):

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

Anne Baanen (May 18 2020 at 11:21):

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

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.

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

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!

Filippo A. E. Nuccio (May 18 2020 at 14:16):

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

Johan Commelin (May 18 2020 at 15:21):

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

Johan Commelin (May 18 2020 at 15:21):

It might be helpful to get that PR merged first

Johan Commelin (May 18 2020 at 15:21):

Because you'll probably benefit from the new localisation API

Anne Baanen (May 18 2020 at 15:24):

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

Johan Commelin (May 18 2020 at 15:25):

Would you mind reviewing the fractional ideal part?

Johan Commelin (May 18 2020 at 15:25):

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

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

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!

Ashwin Iyengar (May 18 2020 at 19:54):

Which may help with the Dedekind domain stuff.

Anne Baanen (May 19 2020 at 08:06):

Great!

Last updated: May 06 2021 at 17:38 UTC