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

[Yaël Dillies]

Riccardo Brasca said:

we should use these two results to define the discriminant as a well defined integer

Did this ever happen?

[Riccardo Brasca]

NumberField.discr

[Yaël Dillies]

And this is the same discriminant as in "discriminant of a quadratic field", right?

[Riccardo Brasca]

Yes, it is what usually people call "the discriminant of a number field" in a first class in number theory.

[Riccardo Brasca]

It's just the discriminant of any ℤ-basis of 𝓞 K. The coincidence is that if you change basis then the discriminant is multiplied by the square of the determinant of the base change matrix (Algebra.discr_of_matrix_vecMul and friends), so for ℤ it's multiplied by 1.

[Yaël Dillies]

For formal-conjectures, I need the characterisation of which integers arise as the discriminant of a quadratic field. I am thinking of either doing it myself or giving it to someone as a beginner project

[Yaël Dillies]

We don't have a definition of "quadratic field". What would such a definition look like? Right now, I am thinking of simply using "QuadraticAlgebra ℚ d 0 for some d ≠ 1 that's Squarefree d"

[Riccardo Brasca]

At ItaLean we computed the ring of integers (not the discriminant). You can find it here.

[Riccardo Brasca]

Yaël Dillies said:

We don't have a definition of "quadratic field". What would such a definition look like? Right now, I am thinking of simply using "QuadraticAlgebra ℚ d 0 for some d ≠ 1 that's Squarefree d"

We took the same approach.

[Riccardo Brasca]

We used the general trace and norm, but one should probably use the version for quadratic algebras (I think the norm is there but not the trace).

[Yaël Dillies]

Wait, there is a quadratic algebra-specific norm?

[Riccardo Brasca]

I mean QuadraticAlgebra.norm

[Riccardo Brasca]

I think in all reasonable cases it's the same as Algebra.norm but it's defined by hand.

[Antoine Chambert-Loir]

Yaël Dillies said:

We don't have a definition of "quadratic field". What would such a definition look like? Right now, I am thinking of simply using "QuadraticAlgebra ℚ d 0 for some d ≠ 1 that's Squarefree d"

I would say NumberField K + finrank Q K = 2.

[Riccardo Brasca]

I think the question here is how to write in Lean "let $K$ be $\mathbb{Q}(\sqrt{d})$", not any quadratic field. IIRC QuadraticAlgebra was introduced exactly for this reason.

[Yaël Dillies]

Actually, I was more thinking of the question that Antoine addressed

[Riccardo Brasca]

I may be wrong, but if you want to compute the discriminant and say something like "it's d or 4d" you need d and it seems easier using QuadraticAlgebra.

[Yaël Dillies]

You are correct for the computation, but at the end I want to wrap the computation up into "The discriminants of quadratic fields are exactly ...", at which point I don't need the d

[Artie Khovanov]

@Yaël Dillies you want docs#Algebra.IsQuadraticExtension

[Yaël Dillies]

I am confused now. There is nothing relating docs#Algebra.IsQuadraticExtension and docs#NumberField. In In particular, just assuming IsQuadraticExtension ℚ K doesn't let me talk about NumberField.discr K. What am I supposed to do?

[Kevin Buzzard]

I guess a general quadratic extension won't be a number field (because it might have nilpotents or it might be Q+Q)

[Yaël Dillies]

But what about a quadratic extension that is also a field?

[Kevin Buzzard]

Then I should think that this is a number field by definition, but I'm not sure I can convince typeclass inference of this because it's the condition that b^2-4ac isn't a square.

[Kevin Buzzard]

NumberField is just a poorly-named Prop, right? So just assume it?

[Yaël Dillies]

Yes, but I was wondering if I could first show more generally that a quadratic extension must be of the form QuadraticAlgebra R a b

[Kevin Buzzard]

Alternatively extend the concept of discriminant to finite separable Q-algebras and then you just have to demand that b^2-4ac isn't zero :-)

I very much for hope that it's true that for any field at all, a quadratic extension must be of this form, because I thought that was the point of QuadraticAlgebra

[Yaël Dillies]

Yes, that's my reasoning too. Proof by name :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

You extend {1} to a basis {1,x} and then write x^2 as a linear combination of the basis elements

[Yaël Dillies]

Maybe the answer is that NumberField.discr gets renamed to Algebra.discr (and generalised), and Algebra discr gets renamed to Algebra.discrBasis?

[Kevin Buzzard]

But a general algebra has no discriminant, maybe it has a discriminant ideal or something. The weird thing about number fields (and more generally finite separable Q-algebras, which is just a pompous way of saying finite products of number fields) is that they have a well-defined integer discriminant. This is exactly why we have NumberField.discr . This is an arithmetic fact, not an algebraic one.

[Antoine Chambert-Loir]

That's why the docs#QuadraticAlgebra.instField has a Fact argument. It would be a reasonable starting point for that project to add the appropriate docs#NumberField instance and prove that, conversely, any number field of degree 2 can be represented (has an docs#AlgEquiv) as a docs#QuadraticAlgebra.

[Antoine Chambert-Loir]

Note that you will not only prove that the number field of degree 2 is a quadratic algebra, but also that its ring of integers is, or that any integral domain which is of rank 2 over the integers is a quadratic algebra.

[Barinder S Banwait]

hi all, wondering what is the latest regarding discriminants of quadratic numbers fields defined via QuadraticAlgebra? i'm trying to verify a particular discriminant as in the following MWE:

import Mathlib

open Polynomial NumberField QuadraticAlgebra RingOfIntegers Algebra

noncomputable section

abbrev f_minpoly : ℚ[X] := X ^ 2 - X + C 2

instance : Fact (Irreducible f_minpoly) := ⟨by
  admit⟩

notation "K" => QuadraticAlgebra ℚ (-2) 1

instance : Fact (∀ (r : ℚ), r ^ 2 ≠ (-2 : ℚ) + (1 : ℚ) * r) := by
  admit

instance : NumberField K := by
  admit

notation "R" => (𝓞 K)
lemma is_integral_ω : IsIntegral ℤ (ω : K) := by
  admit

set_option quotPrecheck false in
notation "θ" => (⟨ω, is_integral_ω⟩ : 𝓞 K)

lemma span_eq_top : adjoin ℤ {θ} = ⊤ := by
  sorry

-- apparently `discr` is the absolute discriminant; will likely use `span_eq_top`
lemma K_discriminant_abs : discr K = 7 := by
  sorry

[Filippo A. E. Nuccio]

Can you explain exactly what you want to achieve here? Are you trying to state that the discriminant of some quadratic field is 7? But what is your long-term goal?

[Barinder S Banwait]

Filippo A. E. Nuccio said:

Can you explain exactly what you want to achieve here? Are you trying to state that the discriminant of some quadratic field is 7? But what is your long-term goal?

Formalising the proof that the absolute discriminant of $\mathbb{Q}(\sqrt{-7})$ equals 7 is the main* last missing piece in my first Lean project of Formalising the proof of the Ramanujan--Nagell theorem. (*: There are some missing details in the proof that the units are just $\pm 1$ which probably won't be too difficult to fill). See the dependency graph there for the status.

That's why I'm quite motivated to know if discriminants of QuadraticAlgebra instances (at least when they're fields) have been done yet, or if they're in progress.

If nobody's working on this, then I'd be happy to do so.

[Riccardo Brasca]

I think @Yaël Dillies was interested in computing the discriminant.

[Yaël Dillies]

Indeed I am (see earlier messages), but I haven't had time to do so yet. I probably won't get to it before another month, so feel free to give it a go!

[Filippo A. E. Nuccio]

For the units, you are aware of NumberField.Units.rank_modTorsion , right?