Enumerating number fields

7 fully proved2 ready to prove

Theorem 1

StructureNumber fields of degree \(n\)#✓fully proved

For a natural number \(n\), the type of number fields of degree \(n\) over \(\mathbb{Q}\): an element is a type \(K\) with a field structure making \(K\) a number field (a field of characteristic zero that is finite-dimensional over \(\mathbb{Q}\)) such that \(\dim_{\mathbb{Q}} K = n\).

structure NumberFieldOfDegree (n : ℕ) where
  /-- The elements of the number field. -/
  carrier : Type
  /-- The field structure of the number field. -/
  field : Field carrier
  numberField : NumberField carrier
  degree : finrank ℚ carrier = n

Used by 3

Used byIsomorphism of number fields with bounded discriminant · Number fields of degree \(n\) with discriminant bounded by \(H\) · Couveignes: number fields have small models

DefinitionQuotient of a polynomial ring by \(r\) polynomials#✓fully proved

For a natural number \(r\) and polynomials \(E_1, \dots, E_r \in \mathbb{Q}[x_1, \dots, x_r]\), the quotient ring \(\mathbb{Q}[x_1, \dots, x_r]/(E_1, \dots, E_r)\) of the polynomial ring by the ideal generated by \(E_1, \dots, E_r\).

def quotientRing : Type :=
  (MvPolynomial (Fin r) ℚ) ⧸ Ideal.span (Set.range E)
deriving CommRing, IsNoetherianRing

Used by 3

Used byJacobian determinant in the quotient ring · The open subscheme where the Jacobian does not vanish · Couveignes: number fields have small models

DefinitionJacobian determinant in the quotient ring#✓fully proved

For polynomials \(E_1, \dots, E_r \in \mathbb{Q}[x_1, \dots, x_r]\), the image in the quotient ring \(\mathbb{Q}[x_1, \dots, x_r]/(E_1, \dots, E_r)\) of the Jacobian determinant \(\det(\partial E_i / \partial x_j)_{1 \le i, j \le r}\).

def jacobian : quotientRing E :=
  Ideal.Quotient.mk _ <| Matrix.det <| fun i j ↦ MvPolynomial.pderiv j (E i)

Uses 1 · Used by 2

Statement usesQuotient of a polynomial ring by \(r\) polynomials

Used byThe open subscheme where the Jacobian does not vanish · Couveignes: number fields have small models

DefinitionThe open subscheme where the Jacobian does not vanish#✓fully proved

For polynomials \(E_1, \dots, E_r \in \mathbb{Q}[x_1, \dots, x_r]\), the open subscheme of \(\operatorname{Spec} \mathbb{Q}[x_1, \dots, x_r]/(E_1, \dots, E_r)\) where the Jacobian determinant \(\det(\partial E_i / \partial x_j)\) does not vanish, that is, the basic open set of the image of this determinant in the quotient ring.

def nonsingularOpen : Scheme :=
  (Spec (.of (quotientRing E))).basicOpen <|
    (ΓSpecIso _).symm.commRingCatIsoToRingEquiv <| jacobian E
deriving IsAffine

Uses 2 · Used by 1

Statement usesJacobian determinant in the quotient ring · Quotient of a polynomial ring by \(r\) polynomials

Used byCouveignes: number fields have small models

TheoremCouveignes: number fields have small models#●ready to prove

There is a positive integer \(Q\) such that for every natural number \(n \ge Q\) and every number field \(K\) of degree \(n\) over \(\mathbb{Q}\), with discriminant \(d_K\) and root discriminant \(\delta_K = |d_K|^{1/n}\), there are natural numbers \(r\) and \(d\) with \(r \le Q \log n\), \(d \le Q \log n\) and \(\binom{d + r}{r} \le Q n \log n\), and polynomials \(E_1, \dots, E_r \in \mathbb{Z}[x_1, \dots, x_r]\) of total degree at most \(d\), all of whose coefficients have absolute value at most \((n \delta_K)^{Q \log n}\), with the following property. Let \(X\) be the open subscheme of \(\operatorname{Spec} \mathbb{Q}[x_1, \dots, x_r]/(E_1, \dots, E_r)\) where \(\det(\partial E_i / \partial x_j) \ne 0\). Then \(X\) has an irreducible component \(Z\) which, with its subscheme structure as the scheme-theoretic closure of the open set of points of \(X\) lying on no other irreducible component, is isomorphic to \(\operatorname{Spec} K\).

public theorem_wanted theorem_1 : ∃ Q > 0, ∀ n ≥ Q, ∀ K : NumberFieldOfDegree n, ∃ (r d : ℕ),
    r ≤ Q * log n ∧ d ≤ Q * log n ∧ (d + r).choose r ≤ Q * n * log n ∧
      ∃ E : Fin r → MvPolynomial (Fin r) ℤ, (∀ i, (E i).totalDegree ≤ d) ∧
        (∀ i j, |(E i).coeff j| ≤ (n * rootDiscr K) ^ (Q * log n)) ∧
          letI X := nonsingularOpen fun i ↦ (E i).map (algebraMap ℤ ℚ)
          ∃ Z, ∃ hZ : Z ∈ irreducibleComponents X,
            Nonempty (X.irreducibleComponent Z hZ ≅ Spec (.of K))

Sources

• J.-M. Couveignes, Enumerating number fields, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_enumerating_number_fields of the lean-eval benchmark.

Uses 4

Statement usesNumber fields of degree \(n\) · Jacobian determinant in the quotient ring · The open subscheme where the Jacobian does not vanish · Quotient of a polynomial ring by \(r\) polynomials

Theorem 2

StructureNumber fields of degree \(n\) with discriminant bounded by \(H\)#✓fully proved

For natural numbers \(n\) and \(H\), the type of number fields \(K\) of degree \(n\) over \(\mathbb{Q}\) whose discriminant \(d_K\) satisfies \(|d_K| \le H\).

structure NumberFieldOfBoundedDiscriminant (n H : ℕ) extends NumberFieldOfDegree n where
  discr : |discr carrier| ≤ H

Uses 1 · Used by 2

Statement usesNumber fields of degree \(n\)

Used byIsomorphism of number fields with bounded discriminant · Isomorphism classes of number fields with bounded discriminant

DefinitionIsomorphism of number fields with bounded discriminant#✓fully proved

For natural numbers \(n\) and \(H\), two number fields \(K\) and \(L\) of degree \(n\) over \(\mathbb{Q}\), each with discriminant of absolute value at most \(H\), are related when there exists a ring isomorphism from \(K\) to \(L\).

def NumberFieldOfBoundedDiscriminant.iso (n H : ℕ) (K L : NumberFieldOfBoundedDiscriminant n H) :=
  Nonempty (K ≃+* L)

Uses 2 · Used by 1

Statement usesNumber fields of degree \(n\) with discriminant bounded by \(H\) · Number fields of degree \(n\)

Used byIsomorphism classes of number fields with bounded discriminant

DefinitionIsomorphism classes of number fields with bounded discriminant#✓fully proved

For natural numbers \(n\) and \(H\), the quotient of the type of number fields of degree \(n\) over \(\mathbb{Q}\) whose discriminant has absolute value at most \(H\) by the relation of being isomorphic as rings.

def NumberFieldOfBoundedDiscriminantUpToIsomorphism (n H : ℕ) :=
  Quot (NumberFieldOfBoundedDiscriminant.iso n H)

Uses 2 · Used by 1

Statement usesNumber fields of degree \(n\) with discriminant bounded by \(H\) · Isomorphism of number fields with bounded discriminant

Used byCouveignes: counting number fields with bounded discriminant

TheoremCouveignes: counting number fields with bounded discriminant#●ready to prove

There is a positive integer \(Q\) such that for all natural numbers \(n \ge Q\) and \(H \ge 1\), there are only finitely many isomorphism classes of number fields of degree \(n\) over \(\mathbb{Q}\) whose discriminant has absolute value at most \(H\), and their number is at most \(n^{Q n (\log n)^3} H^{Q (\log n)^3}\).

public theorem_wanted theorem_2 : ∃ Q > 0, ∀ n ≥ Q, ∀ H ≥ 1,
    Finite (NumberFieldOfBoundedDiscriminantUpToIsomorphism n H) ∧
    (Nat.card (NumberFieldOfBoundedDiscriminantUpToIsomorphism n H) : ℝ) ≤
      n ^ (Q * n * log n ^ 3) * H ^ (Q * log n ^ 3)

Sources

• J.-M. Couveignes, Enumerating number fields, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_enumerating_number_fields of the lean-eval benchmark.

Uses 1

Statement usesIsomorphism classes of number fields with bounded discriminant

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.