class group of a number field

Stream: maths

[Kevin Buzzard]

I've not been thinking about class groups of number fields for a while now, and a number theory PhD student at Imperial has just raised it as a potential Lean project. I think that finiteness of the class group of a number field is within scope, except that as far as I know we don't even have number fields. I know that @Ashvni Narayanan and @Anne Baanen and probably others have been thinking about these things.

1) Number fields. Am I right in thinking that we don't even have the definition yet? Johan and I talked about this once, and came up with the proposal that a number field should just be a field with a Q-algebra structure which is finite-dimensional as a Q-vector space -- all of these are typeclasses.

2) Global fields. The ad hoc definition is that a global field is either a number field or a finite extension of a function field in one variable over a finite field. There is a much much more complex definition which unifies these two cases, which @Adam Topaz told me about, involving fields which have a bunch of valuations on them and satisfy a product formula, but I am not sure that it's worth using that as a definition, it feels more to me like it should be a theorem, and that perhaps it's just worth ignoring function fields for now.

3) Integers of a number field are a Dedekind domain. If we don't have number fields we don't have this, I guess.

4) Integers of a number field have a class group. This is where I begin to get hazy. We have fractional ideals in the generality of integral domains. Do we know that Dedekind domains have class groups yet? I glanced through mathlib but couldn't spot it. Is someone working on this?

5) Class group of a number field is finite. This is a reasonable goal, hopefully. This is mentioned as a "card" at https://github.com/leanprover-community/mathlib/projects/6 . It's not true that the class group of a general Dedekind domain is finite ($$\mathbbb{C}[X,Y]/(Y^2-X^3-1)$$ is a counterexample, it has class group the complex point of the elliptic curve defined by $Y^2=X^3+1$).

It would be nice to get back to this stuff. Finiteness of class group of a number field, and finite generation of the unit group, are two of the theorems we prove in our undergraduate algebraic number theory course, but they don't seem to be on Patrick's list, perhaps because they don't teach them in Orsay.

What is the status of these things?

[Ashvni Narayanan]

To my knowledge, 1, 3, 4 and 5 have been accomplished (or will be, in a few days).

[Ashvni Narayanan]

I have been thinking about 2, I think @Anne Baanen and @Filippo A. E. Nuccio might have more to say on that.

[Kevin Buzzard]

Oh I'm glad I asked! I knew you'd been thinking about this stuff. I'm happy to forget about global fields for now.

[Johan Commelin]

Wow! So even 5 is almost done? That's cool!

[Ashvni Narayanan]

Yes, I think the credit goes majorly to @Anne Baanen :)

[Adam Topaz]

Is Dirichlet's unit theorem also in the works?

[Filippo A. E. Nuccio]

Well, it is "in the works" and I have started thinking a little bit about that. But (as far as I know) nothing has been written and I am probably in the coming future going more in the Liquid Experiment direction, so I would say it is "open".

[Filippo A. E. Nuccio]

Kevin Buzzard said:

I've not been thinking about class groups of number fields for a while now, and a number theory PhD student at Imperial has just raised it as a potential Lean project. I think that finiteness of the class group of a number field is within scope, except that as far as I know we don't even have number fields. I know that Ashvni Narayanan and Anne Baanen and probably others have been thinking about these things.

1) Number fields. Am I right in thinking that we don't even have the definition yet? Johan and I talked about this once, and came up with the proposal that a number field should just be a field with a Q-algebra structure which is finite-dimensional as a Q-vector space -- all of these are typeclasses.

2) Global fields. The ad hoc definition is that a global field is either a number field or a finite extension of a function field in one variable over a finite field. There is a much much more complex definition which unifies these two cases, which Adam Topaz told me about, involving fields which have a bunch of valuations on them and satisfy a product formula, but I am not sure that it's worth using that as a definition, it feels more to me like it should be a theorem, and that perhaps it's just worth ignoring function fields for now.

3) Integers of a number field are a Dedekind domain. If we don't have number fields we don't have this, I guess.

4) Integers of a number field have a class group. This is where I begin to get hazy. We have fractional ideals in the generality of integral domains. Do we know that Dedekind domains have class groups yet? I glanced through mathlib but couldn't spot it. Is someone working on this?

5) Class group of a number field is finite. This is a reasonable goal, hopefully. This is mentioned as a "card" at https://github.com/leanprover-community/mathlib/projects/6 . It's not true that the class group of a general Dedekind domain is finite ($$\mathbbb{C}[X,Y]/(Y^2-X^3-1)$$ is a counterexample, it has class group the complex point of the elliptic curve defined by $Y^2=X^3+1$).

It would be nice to get back to this stuff. Finiteness of class group of a number field, and finite generation of the unit group, are two of the theorems we prove in our undergraduate algebraic number theory course, but they don't seem to be on Patrick's list, perhaps because they don't teach them in Orsay.

What is the status of these things?

Concerning 2), we had a discussion in the Dedekind Domain Project about a "good" definition, but we haven't got that far.

[Adam Topaz]

For 2, I don't remember what definition I mentioned to Kevin, but one possible definition of a global field is a finitely-generated field of Kronecker dimension 1 (and Kronecker dimension can be computed in terms of ranks of valuations).

[Kevin Buzzard]

Adam you pointed out this old paper of Artin and Whaples to me.

[Adam Topaz]

Oh right!

[Adam Topaz]

Actually, I think it was @Alex J. Best that pointed that out.

[Kevin Buzzard]

Oh oops :-) Sorry Alex! It seems to me that in practice it's rather common that arguments split into the number field and function field case. All my stuff with Gee on algebraic reps really needed the Archimedean places, for example

[Anne Baanen]

Johan Commelin said:

Wow! So even 5 is almost done? That's cool!

Here's the relevant declaration in our development branch: https://github.com/leanprover-community/mathlib/blob/dedekind-domain-dev/src/algebraic_number_theory/number_field.lean#L84

[Sander Dahmen]

In fact, it has been set up so that finiteness of the class group for function fields in the easy case, i.e. finite separable extensions of $F(t)$ with $F$ a finite field, should also readily follow.

[Kevin Buzzard]

Is it something like "if all residue fields of a Dedekind domain are finite, then the class group is finite"? Or is there more to it than this?

[Sander Dahmen]

This is not sufficient! There are some crazy counter examples with all residue fields finite and infinite class group I believe (but I would have to look them up)..

[Kevin Buzzard]

Oh interesting! I do not know this stuff at all, I am a number fields guy.

[Sander Dahmen]

Actually me too. But I guess we want to have (somewhat) general stuff in Mathlib..

[Sander Dahmen]

At the end of the day it's some box principle argument that you have to so separately for $\mathbb{Z}$ and $F[t]$ to get some "generalised division with remainder" and then everything works uniformly after that.

[Sander Dahmen]

Except that you still have to do completely inseparable extensions to consider all global fields. If one would actually care about them ;-)

[Adam Topaz]

Finite residue fields + product formula is enough, I think.

[Sander Dahmen]

Could be, do you have a reference? (Does this perhaps translate back from class field theory?)

[Adam Topaz]

This is essentially Artin Whaples (I think... I should check the details there)

[Johan Commelin]

@Anne Baanen @Ashvni Narayanan @Filippo A. E. Nuccio @Sander Dahmen I just finished reading your paper. Really cool project! I didn't realize you covered so much ground! And it's very well-written. This is cool!

[Ashvni Narayanan]

Thank you! :)

[Filippo A. E. Nuccio]

Thanks @Johan Commelin for your nice words.

[Sander Dahmen]

Thanks!

[Anne Baanen]

Thank you :big_smile:

[Kevin Buzzard]

I had some discussions with Ambrus Pal today about this claim in the paper that the result is not complete because it only deals with separable extensions of k(T), k finite. Ambrus says that every smooth irreducible projective curve is a separable cover of P^1, which means that every global function field over a finite field is a separable extension of k(T), meaning that your proof is already complete. He didn't give a precise reference though.

[Adam Topaz]

@Kevin Buzzard this is a general fact about perfect fields.

Wikipedia gives a reference from Matsumura: https://en.m.wikipedia.org/wiki/Perfect_field
(See the section on separating transcendence bases)

[Kevin Buzzard]

Just to be clear, Ambrus did mention the assumption that k was perfect in his email. Yes Matsumura 26.2 does it -- k^{1/p}=k in this finite field setting, and the definition of separably generated is just above theorem 26.1:

matsumura.png

Just to be clear, what I am saying is that 8.2 "Future directions" the first point -- you've done it already, because every global field is of the form you've dealt with.

[Damiano Testa]

I also think that the statement about smooth irreducible projective curves admitting a separable morphism to P^1 is true. It uses the smoothness assumption on the curve. Here is a sketch.

Embed your smooth curve C in projective space via a "sufficiently ample" linear system (any embedding is ok if the field is infinite, which is the only interesting case, as finite fields are perfect anyway).

First, show that there are hyperplanes that intersect the curve C transversely. Indeed, such hyperplanes exist over the algebraic closure of the ground field, since our curve is smooth and hence geometrically reduced. Moreover, the set of such hyperplanes is a dense open subset of the set of all hyperplanes. If our field is infinite, then there are hyperplanes in the intersection. Otherwise, we use a form of Bertini's theorem, exploiting the "ampleness" of the embedding.

Next, use the linear system formed by one hyperplane H transverse to C and any other hyperplane H' ≠ p. This linear system extends to a morphism to ℙ^1 that is separable, since the fiber corresponding to H is geometrically reduced.

The challenge is to formalize a proof of this! :wink:

Here is also an example of what fails otherwise.

Let k be an imperfect field of characteristic p and let k ⊂ k' be a non-separable, purely inseparable extension (i.e. I am excluding the trivial purely inseparable extension!). Let ℙ be ℙ^1 over k', viewed as a scheme over k. Thus, ℙ is a projective curve over k that is not geometrically reduced. Let k ⊂ K be any subfield of the function field k' (x) of ℙ, and let ℙ → C_K be the corresponding morphism of curves. If the morphism ℙ → C_K is separable, then K contains k' and hence C_k is also not geometrically reduced over k`.

Some details are missing, but I am not feeding these results to Lean!

[Damiano Testa]

Oh, I see now that the reference that Kevin gave essentially states a more general version of the statement that I sketched. I leave it here, since I would really like to be able to give such geometric arguments in Lean, doing geometric reductions, before performing simple algebraic computations.

This will take a probably long time, though...

[Kevin Buzzard]

I don't see why it needs to take a long time, we just need people to work on it

[Kevin Buzzard]

Oh here's something else which I knew was true for number fields and only had a vague idea about whether it was true in general: sum of e_i f_i = n. I found this paper https://arxiv.org/abs/2102.10481 (from a few days ago on ArXiv) quite enlightening!

[Adam Topaz]

This is something that's true in general for discrete valuations. general valuations can have "defect" which contradict this.

[Adam Topaz]

I'm sure the book "valued fields" has a textbook account of this

[Kevin Buzzard]

Doesn't Theorem 2 say that this is only true in the Japanese/excellent case?

[Adam Topaz]

I can't seem to open this on my phone right now...

[Adam Topaz]

I'll have to check a little later

[Adam Topaz]

Ok, that's right. It only works for discrete valuations assuming the extension of fields is separable. See https://link.springer.com/book/10.1007/3-540-30035-X section 3.3

[Sander Dahmen]

@Kevin Buzzard @Adam Topaz Still thanks for pointing out Theorem 26.2 in Matsumura etc.!
I guess we should change the first "do to" in our paper to formalizing that a finitely generated field extension over a perfect field $k$ is separably generated over $k$, (and/)or its corollary to global function fields.
(Or we could "cheat" and make the separability part of the function field def., which would be convenient for some purposes, but otherwise quite clumsy to drag around I guess.)

[Kevin Buzzard]

My instinct would be just to say that you've proved it for all global fields (because it's a theorem that you have). This was the same with perfectoid spaces -- along the way we had to put a topology on a perfectoid space and there are two definitions of the topology (generated by X or generated by Y), and a theorem with a very long proof that they're the same, which we didn't formalise. Let's say we put topology X on a perfectoid space. Then what about the papers which claim that the definition is the topology generated by Y? Like you, we chose the definition which made our lives easier.

Definitions are slippery things. If we define an elliptic curve over a field to be a smooth proper geometrically connected variety of dimension 1 with a commutative group structure (which is a definition you'll see in the fancier books) then it will be a lot easier to prove weak Mordell-Weil because we won't have to prove anything about a group law on those pesky plane cubics! Why not just remark that there are several definitions of a global field and they're all known to be mathematically equivalent but you haven't formalised the equivalences, but the issue is only in the char p setting so won't affect your future work?