Counting isomorphism classes

Stream: Is there code for X?

[Kevin Wilson]

Hi all! It's been a bit since I was trying out formalization, and I was curious to try my hand at some (simple) arithmetic statistics. Specifically, I was hoping to formalize Schmidt's result on the number of isomorphism classes of number fields of degree n and discriminant at most X. See https://www.numdam.org/article/AST_1995__228__189_0.pdf

I think the proof details won't be too bad given what's in mathlib today, but I was struggling to actually state the theorem itself.

Specifically, how to define the collection/type/set/... of all isomorphism classes of number fields of a fixed degree and a given discriminant.

I was curious if there were good examples in mathlib or elsewhere of defining such things with an eye toward counting them.

Thanks in advance!

[Bryan Wang]

As for mathlib examples, there is docs#NumberField.finite_of_discr_bdd (Hermite-Minkowski), which seems like it might give a pretty good start.

[Kevin Wilson]

Funny right after I sent this message I found exactly that theorem :-)

Definitely looks like it is a good start! Thank you!

[Kevin Buzzard]

My impression from the paper is that what he actually proves is something like the following: first, given $X$ and $d\geq1$, the number of algebraic integers $\alpha$ in $\mathbb{C}$ (say) such that $\alpha$ has some slightly complicated to write down property is (obviously) $<<X^{(d+2)/4}$, and second that every number field in $\mathbb{C}$ of degree $d$ and discriminant bounded in abs value by $X$ is of the form $\mathbb{Q}(\alpha)$ with $\alpha$ having this property. It's a bit more complicated because actually the main result is counting chains $\mathbb{Q}\subset K_1\subset K_2\subset \cdots \subset K$ but that seems to be the basic idea.

[Kevin Wilson]

Indeed. There are several improvements on these bounds that push this idea further, e.g., Ellenberg-Venkatesh: https://annals.math.princeton.edu/wp-content/uploads/annals-v163-n2-p11.pdf (see the top of Section 2)

[Kevin Wilson]

Since the Minkowski bound is now in Mathlib, that's why I figured this wouldn't be too bad to prove now :-)

[Kevin Buzzard]

It will be a challenging but doable project!