The index and the conductor exponent have the same prime divisors

For an integral primitive element θ of a number field K, two integers measure how far the order ℤ[θ] is from 𝓞 K: the index [𝓞 K : ℤ[θ]] (IntegralPrimitiveElement.index) and the conductor exponent RingOfIntegers.exponent θ, the least positive integer e with e • 𝓞 K ⊆ ℤ[θ]. They are different integers in general, but they have the same prime divisors: the exponent divides the index, since the finite group 𝓞 K / ℤ[θ] is killed by its order, and every prime dividing the order of that group divides its exponent, by Cauchy's theorem.

Combined with the index formula disc (minpoly ℤ θ) = [𝓞 K : ℤ[θ]]² · disc K, this gives the hypothesis of the Kummer–Dedekind theorem in checkable form: a prime not dividing the discriminant of the minimal polynomial does not divide the conductor exponent.

Main results

• RingOfIntegers.exponent_dvd_iff: the conductor exponent of θ divides n exactly when n lies in the conductor of ℤ[θ].
• TauCeti.NumberField.IntegralPrimitiveElement.dvd_index_iff_dvd_exponent: a prime divides the index exactly when it divides the conductor exponent.
• TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_exponent_of_not_dvd_discr_minpoly: a natural number not dividing disc (minpoly ℤ θ) does not divide the conductor exponent.
• TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_conductor_sup_span_eq_top: an integer p ≠ 1 comaximal with the conductor of ℤ[θ] does not divide the index.

References

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

theorem RingOfIntegers.exponent_dvd_iff {K : Type u_1} [Field K] (θ : NumberField.RingOfIntegers K) {n : ℕ} : exponent θ ∣ n ↔ ↑n ∈ conductor ℤ θ

The conductor exponent of θ divides n exactly when n lies in the conductor of ℤ[θ].

theorem TauCeti.NumberField.IntegralPrimitiveElement.exponent_dvd_index {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : RingOfIntegers.exponent ↑θ ∣ θ.index

The conductor exponent of θ divides the index [𝓞 K : ℤ[θ]].

theorem TauCeti.NumberField.IntegralPrimitiveElement.dvd_exponent_of_dvd_index {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) {p : ℕ} [Fact (Nat.Prime p)] (hp : p ∣ θ.index) : p ∣ RingOfIntegers.exponent ↑θ

A prime dividing the index [𝓞 K : ℤ[θ]] divides the conductor exponent of θ.

theorem TauCeti.NumberField.IntegralPrimitiveElement.dvd_index_iff_dvd_exponent {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) {p : ℕ} [Fact (Nat.Prime p)] : p ∣ θ.index ↔ p ∣ RingOfIntegers.exponent ↑θ

Index and exponent have the same prime divisors. A prime divides the index [𝓞 K : ℤ[θ]] exactly when it divides the conductor exponent of θ.

theorem TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_conductor_sup_span_eq_top {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) {p : ℕ} (hp : p ≠ 1) (h : conductor ℤ ↑θ ⊔ Ideal.span {↑p} = ⊤) : ¬p ∣ θ.index

If the conductor of ℤ[θ] in 𝓞 K is comaximal with p ≠ 1, then p does not divide the index [𝓞 K : ℤ[θ]].

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

The checkable Kummer–Dedekind hypothesis. A natural number not dividing the discriminant of minpoly ℤ θ does not divide the conductor exponent of θ.