The power basis of an integral primitive element and its discriminant

An integral primitive element θ of a number field K generates K over ℚ, so its powers 1, θ, …, θ ^ (n - 1) form a ℚ-basis of K, where n = [K : ℚ]. This file packages that basis as a PowerBasis ℚ K and identifies its discriminant with the discriminant of the minimal polynomial of θ over ℤ, cast to ℚ.

Main definitions

• TauCeti.NumberField.IntegralPrimitiveElement.powerBasis: the power basis 1, θ, …, θ ^ (n - 1) of K over ℚ.

Main results

• TauCeti.NumberField.IntegralPrimitiveElement.discr_powerBasis_eq_minpoly_discr: the discriminant of the power basis of θ is the polynomial discriminant of minpoly ℤ θ, cast to ℚ.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §2.

noncomputable def TauCeti.NumberField.IntegralPrimitiveElement.powerBasis {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : PowerBasis ℚ K

The power basis 1, θ, …, θ ^ (n - 1) of K over ℚ attached to an integral primitive element θ, where n = [K : ℚ].

Equations

• θ.powerBasis = PowerBasis.ofAdjoinEqTop ⋯ ⋯

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.powerBasis_gen {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : θ.powerBasis.gen = ↑↑θ

The generator of the power basis of θ is θ.

theorem TauCeti.NumberField.IntegralPrimitiveElement.discr_powerBasis_eq_minpoly_discr {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : Algebra.discr ℚ ⇑θ.powerBasis.basis = (algebraMap ℤ ℚ) (minpoly ℤ ↑θ).discr

The discriminant of the power basis of an integral primitive element is the polynomial discriminant of its minimal polynomial over ℤ, cast to ℚ.