Number field discriminant

This file defines the discriminant of a number field.

Main definitions

• NumberField.discr: the absolute 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

@[reducible, inline]

noncomputable abbrev NumberField.discr (K : Type u_1) [Field K] [NumberField K] : ℤ

The absolute discriminant of a number field.

Equations

• NumberField.discr K = Algebra.discr ℤ ⇑(NumberField.RingOfIntegers.basis K)

theorem NumberField.coe_discr (K : Type u_1) [Field K] [NumberField K] : ↑(NumberField.discr K) = Algebra.discr ℚ ⇑(NumberField.integralBasis K)

theorem NumberField.discr_ne_zero (K : Type u_1) [Field K] [NumberField K] : NumberField.discr K ≠ 0

theorem NumberField.discr_eq_discr (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ (NumberField.RingOfIntegers K)) : Algebra.discr ℤ ⇑b = NumberField.discr K

theorem NumberField.discr_eq_discr_of_algEquiv (K : Type u_1) [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) : NumberField.discr K = NumberField.discr L

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.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 * ↑(FiniteDimensional.finrank ℚ K).factorial / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.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 * ↑(FiniteDimensional.finrank ℚ K).factorial / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * √|↑(NumberField.discr K)|

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

theorem NumberField.abs_discr_gt_two {K : Type u_1} [Field K] [NumberField K] (h : 1 < FiniteDimensional.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 wether 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) : FiniteDimensional.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.

@[simp]

theorem Rat.numberField_discr : NumberField.discr ℚ = 1

The absolute discriminant of the number field ℚ is 1.

theorem NumberField.discr_rat : NumberField.discr ℚ = 1

Alias of Rat.numberField_discr.

---

The absolute discriminant of the number field ℚ is 1.

theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral {ι : Type u_2} {ι' : Type u_3} (K : Type u_1) [Field K] [DecidableEq ι] [DecidableEq ι'] [Fintype ι] [Fintype ι'] [NumberField K] {b : Basis ι ℚ K} {b' : Basis ι' ℚ K} (h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)) (h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)) : Algebra.discr ℚ ⇑b = Algebra.discr ℚ ⇑b'

If b and b' are ℚ-bases of a number field K such that ∀ i j, IsIntegral ℤ (b.toMatrix b' i j) and ∀ i j, IsIntegral ℤ (b'.toMatrix b i j) then discr ℚ b = discr ℚ b'.