Ideal class group

Stream: maths

[Anne Baanen]

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]

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

[Anne Baanen]

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

[Johan Commelin]

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

[Johan Commelin]

It's related but unrelated (-;

[Alex J. Best]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

@Patrick Massot Wow, that sounds pretty hardcore

[Patrick Massot]

This was a course by Christophe Soulé

[Patrick Massot]

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

[Anne Baanen]

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]

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

[Anne Baanen]

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

[Filippo A. E. Nuccio]

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

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

It might be helpful to get that PR merged first

[Johan Commelin]

Because you'll probably benefit from the new localisation API

[Anne Baanen]

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

[Johan Commelin]

Would you mind reviewing the fractional ideal part?

[Johan Commelin]

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

[Anne Baanen]

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

[Ashwin Iyengar]

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]

Which may help with the Dedekind domain stuff.

[Anne Baanen]

Great!