The index formula

For an integral primitive element θ of a number field K, the discriminant of the minimal polynomial of θ over ℤ, the index [𝓞 K : ℤ[θ]] and the discriminant of K are related by

disc (minpoly ℤ θ) = [𝓞 K : ℤ[θ]]² · disc K.

The formula compares the discriminants of two ℚ-bases of K: the power basis 1, θ, …, θ ^ (n - 1), whose discriminant is disc (minpoly ℤ θ) (discr_powerBasis_eq_minpoly_discr), and an integral basis of 𝓞 K, whose discriminant is disc K. The change-of-basis matrix between them has integer entries, and its determinant is ±[𝓞 K : ℤ[θ]] (Submodule.natAbs_det_basis_change); the square of that determinant is the factor relating the two discriminants.

Main results

• TauCeti.NumberField.IntegralPrimitiveElement.discr_minpoly_eq_index_sq_mul_discr: the index formula disc (minpoly ℤ θ) = [𝓞 K : ℤ[θ]]² · disc K.
• TauCeti.NumberField.IntegralPrimitiveElement.index_eq_one_of_squarefree_discr: a squarefree polynomial discriminant forces index 1.
• TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_not_dvd_discr_minpoly: a natural number not dividing disc (minpoly ℤ θ) does not divide the index.
• TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_squarefree_map: a prime modulo which minpoly ℤ θ is squarefree does not divide the index.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, Proposition (2.12).

theorem TauCeti.NumberField.IntegralPrimitiveElement.discr_minpoly_eq_index_sq_mul_discr {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : (minpoly ℤ ↑θ).discr = ↑θ.index ^ 2 * NumberField.discr K

The index formula. For an integral primitive element θ of a number field K, the discriminant of minpoly ℤ θ is the square of the index [𝓞 K : ℤ[θ]] times the discriminant of K.

theorem TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_not_dvd_discr_minpoly {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) {p : ℕ} (hp : ¬↑p ∣ (minpoly ℤ ↑θ).discr) : ¬p ∣ θ.index

A natural number not dividing the discriminant of minpoly ℤ θ does not divide the index [𝓞 K : ℤ[θ]].

theorem TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_squarefree_map {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) {p : ℕ} [Fact (Nat.Prime p)] (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ↑θ))) : ¬p ∣ θ.index

A prime modulo which the minimal polynomial is squarefree does not divide the index. If minpoly ℤ θ is squarefree modulo the prime p, then its discriminant is nonzero modulo p, so p does not divide [𝓞 K : ℤ[θ]] by the index formula.

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_eq_one_of_squarefree_discr {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (hsq : Squarefree (minpoly ℤ ↑θ).discr) : θ.index = 1

A squarefree polynomial discriminant forces index 1. If the discriminant of minpoly ℤ θ is squarefree, then ℤ[θ] = 𝓞 K.