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 (NumberField.mixedEmbedding.latticeBasis K)) = 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(NNReal.sqrt ‖NumberField.discr K‖₊)

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

theorem NumberField.mixedEmbedding.covolume_idealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ZLattice.covolume (NumberField.mixedEmbedding.idealLattice K I) MeasureTheory.volume = ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * √|↑(NumberField.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 (NumberField.RingOfIntegers K)) K)ˣ) : ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|

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

theorem NumberField.abs_discr_gt_two {K : Type u_1} [Field K] [NumberField K] (h : 1 < Module.finrank ℚ K) : 2 < |NumberField.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 : |NumberField.discr K| ≤ ↑N) : Module.finrank ℚ K ≤ NumberField.hermiteTheorem.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 : |NumberField.discr K| ≤ ↑N) : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.hermiteTheorem.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 : |NumberField.discr K| ≤ ↑N) (a : NumberField.RingOfIntegers K) (h : ℚ⟮↑a⟯ = ⊤) : (minpoly ℤ ↑a).natDegree ≤ NumberField.hermiteTheorem.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 : NumberField.InfinitePlace ↥↑K | w.IsReal}.Nonempty ∧ |NumberField.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 : NumberField.InfinitePlace ↥↑K | w.IsComplex}.Nonempty ∧ |NumberField.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 } | |NumberField.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.