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
noncomputable def NumberField.rootDiscr (K : Type u_1) [Field K] [NumberField K] :
โ„

The root discriminant of a number field K.

Instances For
    source
    ๐Ÿ“ coverage
    theorem NumberField.rootDiscr_def (K : Type u_1) [Field K] [NumberField K] :
    rootDiscr K = โ†‘|discr K| ^ (โ†‘(Module.finrank โ„š K))โปยน
    source
    ๐Ÿ“ coverage
    theorem NumberField.rootDiscr_rat :
    rootDiscr โ„š = 1
    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.

    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.

      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.