The discriminant of a number field from an integral basis

If b is (the image in K of) a ℤ-basis of the ring of integers 𝒪_K — an integral basis — then its rational trace-form discriminant is exactly the field discriminant,

disc b = d_K (over ℚ).

More usefully, this holds for any ℚ-basis b of K consisting of algebraic integers whose ℤ-span inside 𝒪_K is everything: exhibiting such a spanning integral basis and evaluating its discriminant computes d_K on the nose. This is the exact-attainment half of the effective discriminant bound |d_K| ≤ |disc b| (NumberField.abs_discr_le_of_basis_isIntegral), which is strict exactly when the span has index m > 1 (then disc b = m² · d_K). It also drives concrete discriminant computations, e.g. {1, i} is a ℤ-basis of the Gaussian integers and disc {1, i} = -4 gives d_{ℚ(i)} = -4.

Main results

• NumberField.discr_eq_of_integralBasis: for a ℤ-basis c of 𝒪_K, the rational discriminant of its image in K equals d_K.
• NumberField.discr_eq_of_basis_isIntegral_of_span_eq_top: the same, phrased for a ℚ-basis b of algebraic integers whose ℤ-span (inside 𝒪_K) is everything.
• NumberField.abs_discr_eq_of_basis_isIntegral_of_span_eq_top: the matching |d_K| = |disc b|, the equality companion of abs_discr_le_of_basis_isIntegral.
• NumberField.discr_eq_of_basis_isIntegral_of_span_eq_top_of_discr_eq_int: the consumer form that turns an evaluated integer basis discriminant into d_K exactly, with NumberField.natAbs_discr_eq_of_basis_isIntegral_of_span_eq_top_of_discr_eq_int its natAbs corollary.

Provenance

No formal code is vendored. The equality is assembled from Mathlib's Algebra.discr_localizationLocalization and NumberField.discr_eq_discr; the ℚ-basis form constructs the ℤ-basis of 𝒪_K from the spanning hypothesis. It is the exact-attainment companion of the migrated Layer-1 bound NumberField.abs_discr_le_of_basis_isIntegral, whose source attribution (kim-em/erdos-unit-distance) is in TauCeti/NumberTheory/EffectiveBounds/Discriminant/Basic.lean.

theorem NumberField.discr_eq_of_integralBasis {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (c : Module.Basis ι ℤ (RingOfIntegers K)) : (Algebra.discr ℚ fun (i : ι) => (algebraMap (RingOfIntegers K) K) (c i)) = ↑(discr K)

An integral basis attains the discriminant bound. For a ℤ-basis c of the ring of integers 𝒪_K, the rational discriminant of the induced ℚ-basis of K is exactly the field discriminant d_K.

theorem NumberField.discr_eq_of_basis_isIntegral_of_span_eq_top {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) (hspan : Submodule.span ℤ (Set.range fun (i : ι) => ⟨b i, ⋯⟩) = ⊤) : Algebra.discr ℚ ⇑b = ↑(discr K)

The discriminant bound is an equality for a spanning integral basis. If b is a ℚ-basis of K consisting of algebraic integers whose ℤ-span inside 𝒪_K is all of 𝒪_K, then disc b = d_K exactly (over ℚ).

theorem NumberField.abs_discr_eq_of_basis_isIntegral_of_span_eq_top {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) (hspan : Submodule.span ℤ (Set.range fun (i : ι) => ⟨b i, ⋯⟩) = ⊤) : |↑(discr K)| = |Algebra.discr ℚ ⇑b|

The equality companion of the effective discriminant bound. For a ℚ-basis of algebraic integers that generates 𝒪_K, the effective bound |d_K| ≤ |disc b| is an equality.

theorem NumberField.discr_eq_of_basis_isIntegral_of_span_eq_top_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)) (hspan : Submodule.span ℤ (Set.range fun (i : ι) => ⟨b i, ⋯⟩) = ⊤) {d : ℤ} (hd : Algebra.discr ℚ ⇑b = ↑d) : discr K = d

Evaluating the discriminant through a spanning integral basis. If the discriminant of a generating basis of algebraic integers computes to an integer d, then d_K = d exactly. This is the consumer form used to read off d_K from a concrete trace-form computation, as in the roadmap's ℚ(i) example (disc {1, i} = -4, whence d_{ℚ(i)} = -4).

theorem NumberField.natAbs_discr_eq_of_basis_isIntegral_of_span_eq_top_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)) (hspan : Submodule.span ℤ (Set.range fun (i : ι) => ⟨b i, ⋯⟩) = ⊤) {d : ℤ} (hd : Algebra.discr ℚ ⇑b = ↑d) : (discr K).natAbs = d.natAbs

The absolute value of the discriminant from a spanning integral basis. The natAbs corollary of discr_eq_of_basis_isIntegral_of_span_eq_top_of_discr_eq_int, reading off |d_K| from an evaluated integer basis discriminant (in the ℚ(i) example, (d_{ℚ(i)}).natAbs = 4).