Documentation

Mathlib.NumberTheory.NumberField.Discriminant.Basic

Number field discriminant #

This file defines the discriminant of a number field.

Main result #

Tags #

number field, discriminant

source
๐Ÿ“ coverage
theorem NumberField.discr_eq_basisMatrix_det_sq (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K โ†’+* โ„‚)] :
โ†‘(discr K) = (basisMatrix K).det ^ 2
source
๐Ÿ“ coverage
theorem NumberField.sign_discr (K : Type u_1) [Field K] [NumberField K] :
(discr K).sign = (-1) ^ InfinitePlace.nrComplexPlaces K
source
๐Ÿ“ coverage
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โ€–โ‚Š)
source
๐Ÿ“ coverage
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)|
source
๐Ÿ“ coverage
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)|
source
๐Ÿ“ coverage
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)|
source
๐Ÿ“ coverage
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)|
source
๐Ÿ“ coverage
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.

source
๐Ÿ“ coverage
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|
source
๐Ÿ“ coverage
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))โปยน
source
๐Ÿ“ coverage
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|
source
๐Ÿ“ coverage
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 an infinite real place or not, the theorem is proved in two parts.

source
๐Ÿ“ coverage
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
source
๐Ÿ”ธ coverage
@[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
    Instances For
      source
      ๐Ÿ”ธ coverage
      @[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
        Instances For
          source
          ๐Ÿ“ coverage
          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.

          source
          ๐Ÿ“ coverage
          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.

          source
          ๐Ÿ“ coverage
          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
          source
          ๐Ÿ“ coverage
          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
          source
          ๐Ÿ“ coverage
          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
          source
          ๐Ÿ“ coverage
          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.