Documentation

Mathlib.NumberTheory.NumberField.Discriminant

Number field discriminant #

This file defines the discriminant of a number field.

Main definitions #

Main result #

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
Instances For

    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 AProp} (S : Set { F : IntermediateField A // p F }) {T : Set A} (hT : T.Finite) (h : FS, xT, F = x) :
    S.Finite
    @[reducible, inline]

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

    Equations
    Instances For
      @[reducible, inline]

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

      Equations
      Instances For

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

        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]

        The absolute discriminant of the number field is 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)) :

        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'.