Number field discriminant

This file defines the discriminant of a number field.

Main result

• NumberField.abs_discr_gt_two: Hermite-Minkowski Theorem. A nontrivial number field has discriminant greater than 2.

• NumberField.finite_of_discr_bdd: Hermite Theorem. Let N be an integer. There are only finitely many number fields (in some fixed extension of ℚ) of discriminant bounded by N.

Tags

number field, discriminant

theorem NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.volume (ZSpan.fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(NNReal.sqrt ‖discr K‖₊)

theorem NumberField.mixedEmbedding.covolume_integerLattice (K : Type u_1) [Field K] [NumberField K] : ZLattice.covolume (mixedEmbedding.integerLattice K) MeasureTheory.volume = 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * √|↑(discr K)|

theorem NumberField.mixedEmbedding.covolume_idealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ZLattice.covolume (idealLattice K I) MeasureTheory.volume = ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * √|↑(discr K)|

theorem NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(discr K)|

theorem NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr (K : Type u_1) [Field K] [NumberField K] : ∃ (a : RingOfIntegers K), a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (4 / Real.pi) ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(discr K)|

theorem NumberField.abs_discr_ge' (K : Type u_1) [Field K] [NumberField K] : ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) / ((4 / Real.pi) ^ (2 * InfinitePlace.nrComplexPlaces K) * ↑(Module.finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

The Minkowski lower bound n^{2n}/((4/pi)^{2r_2}*n!^2) for the absolute value of the discriminant of a number field of degree n.

theorem NumberField.abs_discr_ge_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) / ((4 / Real.pi) ^ Module.finrank ℚ K * ↑(Module.finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

theorem NumberField.abs_discr_rpow_ge_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : ↑(Module.finrank ℚ K) ^ 2 / (4 / Real.pi * ↑(Module.finrank ℚ K).factorial ^ (2 * (↑(Module.finrank ℚ K))⁻¹)) ≤ ↑|discr K| ^ (↑(Module.finrank ℚ K))⁻¹

theorem NumberField.abs_discr_ge {K : Type u_1} [Field K] [NumberField K] (h : 1 < Module.finrank ℚ K) : 4 / 9 * (3 * Real.pi / 4) ^ Module.finrank ℚ K ≤ ↑|discr K|

theorem NumberField.abs_discr_gt_two {K : Type u_1} [Field K] [NumberField K] (h : 1 < Module.finrank ℚ K) : 2 < |discr K|

Hermite-Minkowski Theorem. A nontrivial number field has discriminant greater than 2.

Hermite Theorem

This section is devoted to the proof of Hermite theorem.

Let N be an integer . We prove that the set S of finite extensions K of ℚ (in some fixed extension A of ℚ) such that |discr K| ≤ N is finite by proving, using finite_of_finite_generating_set, that there exists a finite set T ⊆ A such that ∀ K ∈ S, ∃ x ∈ T, K = ℚ⟮x⟯ .

To find the set T, we construct a finite set T₀ of polynomials in ℤ[X] containing, for each K ∈ S, the minimal polynomial of a primitive element of K. The set T is then the union of roots in A of the polynomials in T₀. More precisely, the set T₀ is the set of all polynomials in ℤ[X] of degrees and coefficients bounded by some explicit constants depending only on N.

Indeed, we prove that, for any field K in S, its degree is bounded, see rank_le_rankOfDiscrBdd, and also its Minkowski bound, see minkowskiBound_lt_boundOfDiscBdd. Thus it follows from mixedEmbedding.exists_primitive_element_lt_of_isComplex and mixedEmbedding.exists_primitive_element_lt_of_isReal that there exists an algebraic integer x of K such that K = ℚ(x) and the conjugates of x are all bounded by some quantity depending only on N.

Since the primitive element x is constructed differently depending on whether K has a infinite real place or not, the theorem is proved in two parts.

theorem NumberField.hermiteTheorem.finite_of_finite_generating_set (A : Type u_2) [Field A] [CharZero A] {p : IntermediateField ℚ A → Prop} (S : Set { F : IntermediateField ℚ A // p F }) {T : Set A} (hT : T.Finite) (h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯) : S.Finite

@[reducible, inline]

noncomputable abbrev NumberField.hermiteTheorem.rankOfDiscrBdd (N : ℕ) : ℕ

An upper bound on the degree of a number field K with |discr K| ≤ N, see rank_le_rankOfDiscrBdd.

Equations

• NumberField.hermiteTheorem.rankOfDiscrBdd N = max 1 ⌊Real.log (9 / 4 * ↑N) / Real.log (3 * Real.pi / 4)⌋₊

@[reducible, inline]

noncomputable abbrev NumberField.hermiteTheorem.boundOfDiscBdd (N : ℕ) : NNReal

An upper bound on the Minkowski bound of a number field K with |discr K| ≤ N; see minkowskiBound_lt_boundOfDiscBdd.

Equations

• NumberField.hermiteTheorem.boundOfDiscBdd N = NNReal.sqrt ↑N * 2 ^ NumberField.hermiteTheorem.rankOfDiscrBdd N + 1

theorem NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd {K : Type u_1} [Field K] [NumberField K] {N : ℕ} (hK : |discr K| ≤ ↑N) : Module.finrank ℚ K ≤ rankOfDiscrBdd N

If |discr K| ≤ N then the degree of K is at most rankOfDiscrBdd.

theorem NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd {K : Type u_1} [Field K] [NumberField K] {N : ℕ} (hK : |discr K| ≤ ↑N) : mixedEmbedding.minkowskiBound K 1 < ↑(boundOfDiscBdd N)

If |discr K| ≤ N then the Minkowski bound of K is less than boundOfDiscrBdd.

theorem NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd {K : Type u_1} [Field K] [NumberField K] {N : ℕ} (hK : |discr K| ≤ ↑N) (a : RingOfIntegers K) (h : ℚ⟮↑a⟯ = ⊤) : (minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N

theorem NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal (A : Type u_2) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | {w : InfinitePlace ↥↑K | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}.Finite

theorem NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex (A : Type u_2) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | {w : InfinitePlace ↥↑K | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}.Finite

theorem NumberField.finite_of_discr_bdd (A : Type u_2) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |discr ↥↑K| ≤ ↑N}.Finite

Hermite Theorem. Let N be an integer. There are only finitely many number fields (in some fixed extension of ℚ) of discriminant bounded by N.