An effective discriminant bound from a basis of algebraic integers

For a number field K, the discriminant of any ℚ-basis consisting of algebraic integers is a nonzero-integer-square multiple of the field discriminant d_K, so it bounds |d_K| from above:

|d_K| ≤ |disc b| for every ℚ-basis b of 𝒪_K-integers.

This is the elementary upper half of the effective-bounds roadmap (the deep content is the matching Minkowski lower bound).

Main results

• NumberField.abs_discr_le_of_basis_isIntegral: |d_K| ≤ |disc b| for a ℚ-basis b consisting of algebraic integers.

The remaining declarations are its consumer forms, converting the rational basis-discriminant bound into the natural-number and integer-absolute-value shapes that concrete trace-form computations (for example the roadmap's ℚ(i) worked example) carry: abs_discr_le_of_basis_isIntegral_of_abs_discr_le, natAbs_discr_le_of_basis_isIntegral_of_discr_eq_int and its _of_natAbs_le/_eq_nat variants, and abs_discr_le_int_of_basis_isIntegral_of_discr_eq_int_of_natAbs_le.

The final section evaluates the bound on a quadratic square-root field: for K = ℚ(x) with x² = a ∈ ℤ and x ∉ ℚ, the {1, x} trace-form discriminant is 4·a, giving the closed form |d_K| ≤ 4·|a| (abs_discr_le_of_sq_intCast, and its integer form abs_discr_le_int_of_sq_intCast). This is the tool the roadmap's quadratic worked examples need: ℚ(i) (a = -1) gives |d_K| ≤ 4, and ℚ(√-5) (a = -5) gives |d_K| ≤ 20.

Provenance

The general algebraic-integer basis discriminant bound was migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where this was a discriminant input to a class-number bound; the statement holds over an arbitrary number field. The quadratic closed-form bounds are local compositions of this bound with the trace-form calculation for a square-root basis.

theorem NumberField.abs_discr_le_of_basis_isIntegral {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) : |↑(discr K)| ≤ |Algebra.discr ℚ ⇑b|

If b is a ℚ-basis of a number field K consisting of algebraic integers, then |d_K| ≤ |disc b|.

theorem NumberField.abs_discr_le_of_basis_isIntegral_of_abs_discr_le {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) {B : ℚ} (hB : |Algebra.discr ℚ ⇑b| ≤ B) : |↑(discr K)| ≤ B

If the discriminant of an algebraic-integer basis is bounded by B, then the number-field discriminant is bounded by the same rational number.

theorem NumberField.natAbs_discr_le_of_basis_isIntegral_of_discr_eq_int {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) {d : ℤ} (hdisc : Algebra.discr ℚ ⇑b = ↑d) : (discr K).natAbs ≤ d.natAbs

If the trace-form discriminant of an algebraic-integer basis computes to the integer d, then the natural absolute discriminant of the number field is at most d.natAbs.

theorem NumberField.natAbs_discr_le_of_basis_isIntegral_of_discr_eq_int_of_natAbs_le {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) {d : ℤ} {D : ℕ} (hdisc : Algebra.discr ℚ ⇑b = ↑d) (hd : d.natAbs ≤ D) : (discr K).natAbs ≤ D

If the trace-form discriminant of an algebraic-integer basis computes to the integer d, and d.natAbs ≤ D, then (NumberField.discr K).natAbs ≤ D.

theorem NumberField.natAbs_discr_le_of_basis_isIntegral_of_discr_eq_nat {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) {D : ℕ} (hdisc : Algebra.discr ℚ ⇑b = ↑D) : (discr K).natAbs ≤ D

If the trace-form discriminant of an algebraic-integer basis computes to the natural number D, then (NumberField.discr K).natAbs ≤ D.

theorem NumberField.abs_discr_le_int_of_basis_isIntegral_of_discr_eq_int_of_natAbs_le {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) {d : ℤ} {D : ℕ} (hdisc : Algebra.discr ℚ ⇑b = ↑d) (hd : d.natAbs ≤ D) : |discr K| ≤ ↑D

If the trace-form discriminant of an algebraic-integer basis computes to an integer d with d.natAbs ≤ D, the same natural-number discriminant bound may be read as an integer absolute-value bound.

theorem NumberField.abs_discr_le_of_sq_intCast {K : Type u_1} [Field K] [NumberField K] {x : K} {a : ℤ} (hfin : Module.finrank ℚ K = 2) (hx2 : x ^ 2 = (algebraMap ℤ K) a) (hx : x ∉ (algebraMap ℚ K).range) : |↑(discr K)| ≤ 4 * |↑a|

For a quadratic number field K and an element x : K whose square is an integer a and which is not rational, the field discriminant satisfies |d_K| ≤ 4·|a|.

theorem NumberField.abs_discr_le_int_of_sq_intCast {K : Type u_1} [Field K] [NumberField K] {x : K} {a : ℤ} (hfin : Module.finrank ℚ K = 2) (hx2 : x ^ 2 = (algebraMap ℤ K) a) (hx : x ∉ (algebraMap ℚ K).range) : |discr K| ≤ 4 * |a|

The integer form of the quadratic discriminant bound: |d_K| ≤ 4·|a| over ℤ, for a quadratic field K with x² = a ∈ ℤ and x ∉ ℚ.