Discriminant of a number field

Stream: maths

[Riccardo Brasca]

To work on flt-regular we will need the discriminant of a number field. The usual definition uses embeddings in the complex numbers.

I propose to define it as the determinant of the matrix given by the trace of all the products of an integral basis of the ring of integers.

Any ideas about this definition?

[Riccardo Brasca]

Note that we already have docs#algebra.trace

[Chris Birkbeck]

This I guess would be an easy way to define it, but having the embedding definition is handy for proving things about discriminants. So I'm not sure if we've just made our proofs more annoying (although maybe for flt_regular we can get away with it).

[Riccardo Brasca]

The problem with the other definition is that we have to choose an algebraic closure (or work inside C) from the beginning. But if at some point we want to add something to our base field, like the root of a polynomial and we use docs#adjoin_root, we are note anymore in the same algebraic closure. We can of course add the relevant root from the algebraic closure, but we don't have the API for adjoint_root.

[Kevin Buzzard]

It might not be relevant for flt-regular but at some point we'll need the theorem saying the rank of the unit group is $r+s-1$ and we'll need embeddings in the complexes for this too.

[Riccardo Brasca]

Sure, sooner or later embeddings are needed for algebraic number theory. But a number field is not a subfield of C, so it seems quite unnatural to work only in C.

[Kevin Buzzard]

One also wants the concept of the determinant of an $n$-tuple (e.g. isn't this the way one proves that certain rings are the full ring of integers, you find a potential ring of integers, like $\mathbb{Z}[\alpha]$ in some $\mathbb{Q}(\alpha)$, compute the discriminant of the $n$-tuple $\{1,\alpha,\alpha^2,\ldots\}$, and then argue that if the ring were any bigger then its discriminant would not be an integer).

[Kevin Buzzard]

How do Pari and LMFDB do it? I doubt they use complexes. I think the determinant of the trace form is a fine idea.

[Chris Birkbeck]

Kevin Buzzard said:

One also wants the concept of the determinant of an $n$-tuple (e.g. isn't this the way one proves that certain rings are the full ring of integers, you find a potential ring of integers, like $\mathbb{Z}[\alpha]$ in some $\mathbb{Q}(\alpha)$, compute the discriminant of the $n$-tuple $\{1,\alpha,\alpha^2,\ldots\}$, and then argue that if the ring were any bigger then its discriminant would not be an integer).

You can still do this with this Ricardo's definition, just take the det of the matrix of traces of the products of the elements.

[Riccardo Brasca]

Exactly, this works out of the box for a tuple of elements in a R-algebra A, without any assumption.

[Kevin Buzzard]

I guess that to take the trace you need finitely generated and projective (maybe finitely presented in the non-Noetherian case)

[Riccardo Brasca]

noncomputable def trace : S →ₗ[R] R :=
(linear_map.trace R S).comp (lmul R S).to_linear_map

No assumptions :big_smile:

[Riccardo Brasca]

It's probably not very well behaved in general, but it's there.

[Kevin Buzzard]

?! Does it give the right thing in a projective non-free example?

[Kevin Buzzard]

Not that it matters for fields, but still...

[Kevin Buzzard]

/-- Trace of an endomorphism independent of basis. -/
def trace : (M →ₗ[R] M) →ₗ[R] R :=
if H : ∃ (s : finset M), nonempty (basis s R M)
then trace_aux R H.some_spec.some
else 0

youch

[Kevin Buzzard]

the definition should have a health warning

[Riccardo Brasca]

:scream:

[Kevin Buzzard]

@Anne Baanen I know you're on holiday so this can definitely wait. If $A\to B$ is a morphism of commutative rings and $B$ is not a finite free $A$-module but if it is _locally_ finite free (for example a non-zero ideal of a Dedekind domain is not always principal i.e. free but it is always locally free of rank 1) then there's still a notion of trace, which will be used by people in the algebra community. On the other hand what we currently have covers most usages of the word (but perhaps not what we want in this thread, if we start doing traces from $B$ to $A$ if $B$ is the integers in a number field and $A$ is the integers in a smaller number field). I guess also there is a notion of trace in the theory of Banach spaces, where the endomorphisms are of infinite-dimensional spaces but there might be a good notion of trace anyway (morally the sum of the eigenvalues happens to converge). Maybe this is just an unsolvable problem -- maybe the algebraists / algebraic number theorists need to define relative_trace or something, and the Banach space people need to define banach_trace ...

[Chris Birkbeck]

Kevin Buzzard said:

How do Pari and LMFDB do it? I doubt they use complexes. I think the determinant of the trace form is a fine idea.

I expect they compute an integral basis and then use the trace form. Computing the discriminant of the defining polynomial can be done without embeddings by using resultants and from there I think one can start to generate the integral basis.

[Antoine Chambert-Loir]

@Kevin Buzzard For infinite dimensional spaces, you indeed have (at least) two notions of traces:

1. The algebraic one, for endomorphisms of finite rank.
2. For (say Banach) spaces, analytic one, defined on the subspace of “endomorphisms with finite trace”, which are limits of operators of finite rank, defined by a formula $\sum a_i f_i \otimes e_i$ (where $(a_i)$ is a summable family of scalars, $f_i$ an bounded family of linear forms, $e_i$ a bounded family of vectors), and the trace is $\sum a_i f_i(e_i)$.

In Hilbert spaces, (2) coincides with the linear span of hermitian endomorphisms whose sum of eigenvalues converges.

[Chris Birkbeck]

Kevin Buzzard said:

It might not be relevant for flt-regular but at some point we'll need the theorem saying the rank of the unit group is $r+s-1$ and we'll need embeddings in the complexes for this too.

We might even need it here. At some point, the proofs I've seen use something like "An algebraic integer all of whose conjugates have absolute value one is a root of unity" and I'm not sure if you get away without using embeddings. But I could be wrong.

[Kevin Buzzard]

Yes you need embeddings for that, or all the infinite norms

[Dima Pasechnik]

Chris Birkbeck said:

Kevin Buzzard said:

How do Pari and LMFDB do it? I doubt they use complexes. I think the determinant of the trace form is a fine idea.

I expect they compute an integral basis and then use the trace form. Computing the discriminant of the defining polynomial can be done without embeddings by using resultants and from there I think one can start to generate the integral basis.

Sage's NumberField definitely doesn't need an embedding to give you its discriminant.

[Riccardo Brasca]

In flt-regular we went for the definition that uses the trace. Here is a proof that this is the same as using embeddings.

[Riccardo Brasca]

docs#algebra.discr has now a reasonable API, and, with #11396, mathlib will know that the discriminant is integral.

I wrote this for the flt-regular project, and I think I have proved more or less the results we need there (we computed the discriminant of the p-th cyclotomic field). If someone is looking for a good first project I think it would be very nice to develop the API for the discriminant of a number field, rather than of a family of vectors, as a well defined integer. All the relevant results are already there so it shouldn't be too difficult. I don't think we need this so I am not going to work on it anytime soon.

[Yaël Dillies]

cc @Elias Caeiro

[Riccardo Brasca]

And of course then we will want arithmetic of quadratic fields!

[Yaël Dillies]

I can't cc them twice :laughing:

[Alex J. Best]

@Riccardo Brasca how about adding this project (or two projects) as a github issue? Maybe as part of https://github.com/leanprover-community/mathlib/projects/3

[Riccardo Brasca]

Good idea!

[Riccardo Brasca]

Done

[Kevin Buzzard]

What's the sign of this "well-defined integer"? Is there ambiguity in the literature?

[David Wärn]

It depends on the number field. The discriminant scales by determinant-squared under change of basis, so the discriminant of a number field is well-defined modulo $(\Z^\times)^2 = \{1\}$

[Kevin Buzzard]

That doesn't stop there being ambiguity in the literature

[Johan Commelin]

So you're asking how the literature scales under change of author?

[Kevin Buzzard]

I guess we make the sensible choice and hope that most other people do too. In the relative setting the discriminant can only be defined as an ideal but as David says in the absolute situation there seems to be a canonical generator

[Kevin Buzzard]

It would be interesting to start writing down solutions to Mordell equations y^2=x^3+n for small nonzero integers. Each equation only has finitely many integer solutions but as n increases so do the amount of techniques that one needs to solve them

[Kevin Buzzard]

IIRC I set a nasty one of these as a codewars kata

[Riccardo Brasca]

The sign is $(-1)^{r_2}$, isn't it? (Here $r_2$ is the number of complex places of $K$.)

[Riccardo Brasca]

Note that I am talking about the discriminant $K/\mathbb{Q}$, I don't see any ambiguity here: take any algebraic integer $x$ such that $K=\mathbb{Q}(x)$ and then set $\Delta_{K/\mathbb{Q}}=\operatorname{discr}(1,x,\ldots,x^{d-1})$, where $d=\dim_{\mathbb{Q}}(K)$.

[Kevin Buzzard]

Right. I'm just familiar with the general theory, where the discriminant is usually define as an ideal of the bottom ring, and the different (in the LCI case) as an ideal of the top ring

[Kevin Buzzard]

I don't think I'd ever internalised that in the absolute case the ideal had a canonical generator. Most of the more advanced results about discriminant are only about primes dividing it or its absolute value, and here the sign doesn't matter

[Riccardo Brasca]

I certainly agree that the real discriminant is an ideal, and sooner or later we will need it... time to have the trace of for projective modules I guess!

[Xavier Roblot]

I am reviving this old topic, since I added PR #6394 as an attempt at defining the discriminant of a number field. In this PR, it is defined classically as the discriminant of a ℤ-basis of the ring of integers with an additional result to prove that it does not depend on the choice of the basis. However, @Riccardo Brasca suggested that maybe the discriminant should be defined as an ideal and not an integer. You can see our discussion there. Still, we thought it would be a good idea to ask for some more opinions here.

[Yaël Dillies]

"a good ideal" :grinning_face_with_smiling_eyes:

[Johan Commelin]

I think we need both: the discriminant as ideal, and the absolute discriminant as integer. And the glue: ideals in Z are the same as natural numbers.

[Xavier Roblot]

Johan Commelin said:

I think we need both: the discriminant as ideal, and the absolute discriminant as integer. And the glue: ideals in Z are the same as natural numbers.

I agree except that I would call relative discriminant the one that is an ideal and (absolute) discriminant the one that is an integer to stick with the usual convention: see https://en.wikipedia.org/wiki/Discriminant_of_an_algebraic_number_field

[David Loeffler]

Johan Commelin said:

I think we need both: the discriminant as ideal, and the absolute discriminant as integer. And the glue: ideals in Z are the same as natural numbers.

We will definitely want both: the absolute discriminant has a well-defined sign, which can't be recovered from the discriminant as an ideal (and this sign carries interesting information – if you just take the absolute values everywhere, you lose the rather elegant theorem that discriminants of number fields are always 0 or 1 mod 4).

[Johan Commelin]

Aah, of course! Yes, you're right.

[Riccardo Brasca]

My main concern is not about having it as an ideal or an integer: it is about defining it using a Z basis or a Q basis made of integral elements (I am on mobile sorry). I have the impression that what we do mathematically is the former option (for example we often compute the discriminant before computing the ring of integers).

[Riccardo Brasca]

For example for cyclotomic fields we do exactly this: we compute the discriminant of the field, and we use it to describe the ring of integers.

[Kevin Buzzard]

Surely we need both; relative discriminant as an ideal of the integers of the bottom field for a finite extension of global fields (and can't this definition be made in some huge generality for finite locally free extensions of comm rings) (and also different as ideal of top ring of integers?) and also absolute discriminant as a number for number fields over Q

[David Loeffler]

@Kevin you seem to be answering the previous question :-)

If I understand Riccardo's point: it's probably going to be useful to have the definition (and some properties) of the discriminant of a specific Q-basis of K, without assuming a priori that this basis is a Z-basis of $O_K$ (because then we can use discriminants as a tool to actually compute $O_K$). And for this, we need a version of discriminant as an actual number – applying generalities about locally free ring extensions will just give us an ideal of $\mathbb{Q}$, which is not terribly useful.

[Xavier Roblot]

David Loeffler said:

If I understand Riccardo's point: it's probably going to be useful to have the definition (and some properties) of the discriminant of a specific Q-basis of K, without assuming a priori that this basis is a Z-basis of $O_K$ (because then we can use discriminants as a tool to actually compute $O_K$). And for this, we need a version of discriminant as an actual number – applying generalities about locally free ring extensions will just give us an ideal of $\mathbb{Q}$, which is not terribly useful.

But isn't it what docs#Algebra.discr does?

[Riccardo Brasca]

Yes, let's forget about ideals for the moment, I agree the absolute discriminant is a number. If you use docs#Algebra.discr you get a rational number, but there is a result saying it is integral if the basis is made of integral elements, and another one saying that it does not depend on the basis (I am still on mobile...). I think we should use these two results to define the discriminant as a well defined integer.

[Xavier Roblot]

When you say basis, you mean basis of what? The discriminant does not depend of the bases if they define the same order. The discriminant of a basis of algebraic integers is the discriminant of the field iff it is a basis of the maximal order. I am afraid I do not understand what you mean...

In any case, it is not necessary to make a quick decision for this PR. We can wait until you are back in front of a computer if it's easier for you.

[Riccardo Brasca]

Maybe I don't remember your definition, but you use a Z basis of O K, right? My proposition is to use a Q basis of K made of integral elements, using https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Discriminant.html#Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral

[Riccardo Brasca]

Mmh, wait, we need that the change of basis is integral, so in practice it looks like a Z basis of O K

[Riccardo Brasca]

In any case I think it is important to have some result that makes possibile to compute the absolute discriminant without knowing what O K is

[Riccardo Brasca]

It's possible I am confused by what is done for cyclotomic fields: I thought the strategy to compute O K in this case is "the discriminant is p^..., then the minimal polynomial of a certain generator is eiseinstein at p, so blah blah". But I now realize the at the beginning we don't know that p^... is the actual discriminant of the ring of integers, but rather of the order given by the primitive root

[Riccardo Brasca]

In particular your definition is absolutely correct, sorry for all the noise

[Xavier Roblot]

Riccardo Brasca said:

In particular your definition is absolutely correct, sorry for all the noise

No problem :smile:

[Antoine Chambert-Loir]

I would say that discriminant and different are also defined for orders, as ideals, compatibly with localization. When ground field is Q, more happens. ..