Common index divisors

A prime p is a common index divisor of a number field K when it divides the index [𝓞 K : ℤ[θ]] of every integral primitive element θ. Such a prime obstructs monogenicity: 𝓞 K = ℤ[θ] would force index θ = 1.

The obstruction is a counting argument. Kummer–Dedekind puts the primes of 𝓞 K above p in bijection with the distinct monic irreducible factors of minpoly ℤ θ modulo p, matching the residue degree of a prime with the degree of its factor — but only for a θ whose conductor exponent is prime to p. So if p has more primes of residue degree d than there are monic irreducible polynomials of degree d available over 𝔽_p, no θ can satisfy that hypothesis, and then p divides exponent θ, hence index θ.

Main definitions

• TauCeti.NumberField.IsCommonIndexDivisor: p divides the index of every integral primitive element.
• TauCeti.NumberField.primesOverOfInertiaDeg: the primes above p of a fixed residue degree.

Main results

• TauCeti.NumberField.IsCommonIndexDivisor.dvd_index: the elimination form, extracting the divisibility at a given integral primitive element.
• TauCeti.NumberField.IsCommonIndexDivisor.not_exists_index_eq_one: a common index divisor rules out an element of index 1, so it obstructs monogenicity.
• TauCeti.NumberField.IsCommonIndexDivisor.adjoin_ne_top: equivalently, no order ℤ[θ] is all of 𝓞 K.
• TauCeti.NumberField.ncard_primesOverOfInertiaDeg_le: the Kummer–Dedekind counting bound.
• TauCeti.NumberField.card_filter_monicFactorsMod_le: the factors of minpoly ℤ θ of degree d are among the degree-d monic irreducibles over 𝔽_p.
• TauCeti.NumberField.isCommonIndexDivisor_of_ncard_lt_ncard: the counting obstruction.

The converse is Hensel's criterion — the common index divisors are exactly the primes whose splitting type is not realizable modulo p — and is deliberately not proved here.

References

• [J. Neukirch, Algebraic number theory][Neukirch1992], III §2 Exercise 1.

def TauCeti.NumberField.IsCommonIndexDivisor (p : ℕ) (K : Type u_2) [Field K] [NumberField K] : Prop

p is a common index divisor of K when it divides the index [𝓞 K : ℤ[θ]] of every integral primitive element θ of K.

A common index divisor obstructs monogenicity. If K admits no integral primitive element the condition holds vacuously, so the predicate carries content only when such a θ exists.

theorem TauCeti.NumberField.isCommonIndexDivisor_iff {K : Type u_1} [Field K] [NumberField K] {p : ℕ} : IsCommonIndexDivisor p K ↔ ∀ (θ : IntegralPrimitiveElement K), p ∣ θ.index

Being a common index divisor is exactly divisibility of every index. The body of IsCommonIndexDivisor is not exposed across module boundaries, so this is the characterisation downstream code uses to prove the predicate or to extract a divisibility from it.

theorem TauCeti.NumberField.IsCommonIndexDivisor.dvd_index {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (h : IsCommonIndexDivisor p K) (θ : IntegralPrimitiveElement K) : p ∣ θ.index

A common index divisor divides every index. The elimination form of the predicate: it extracts the divisibility at a given integral primitive element, so a consumer never has to unfold a definition whose body is not exposed across module boundaries.

theorem TauCeti.NumberField.IsCommonIndexDivisor.not_exists_index_eq_one {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : p ≠ 1) (h : IsCommonIndexDivisor p K) : ¬∃ (θ : IntegralPrimitiveElement K), θ.index = 1

A common index divisor obstructs monogenicity. No integral primitive element has index 1, since p divides every index and p ≠ 1.

Primality is not needed: any p ≠ 1 dividing every index gives the same obstruction.

theorem TauCeti.NumberField.IsCommonIndexDivisor.adjoin_ne_top {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : p ≠ 1) (h : IsCommonIndexDivisor p K) (θ : IntegralPrimitiveElement K) : θ.adjoin ≠ ⊤

The same obstruction stated on orders: no ℤ[θ] generated by an integral primitive element is all of 𝓞 K.

def TauCeti.NumberField.primesOverOfInertiaDeg (K : Type u_1) [Field K] (p d : ℕ) : Set ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K))

The primes of 𝓞 K above p whose residue degree over ℤ is d.

@[simp]

theorem TauCeti.NumberField.mem_primesOverOfInertiaDeg_iff {K : Type u_1} [Field K] (p : ℕ) {d : ℕ} {Q : ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K))} : Q ∈ primesOverOfInertiaDeg K p d ↔ (↑Q).inertiaDeg ℤ = d

Membership in primesOverOfInertiaDeg is the residue-degree condition defining it.

theorem TauCeti.NumberField.card_filter_monicFactorsMod_le {K : Type u_1} [Field K] (p : ℕ) [Fact (Nat.Prime p)] {θ : NumberField.RingOfIntegers K} (d : ℕ) : {Q ∈ RingOfIntegers.monicFactorsMod θ p | Q.natDegree = d}.card ≤ (Polynomial.monicIrreduciblesOfDegree (ZMod p) d).ncard

The degree-d monic irreducible factors of minpoly ℤ θ modulo p are among the degree-d monic irreducibles over 𝔽_p, so they are no more numerous.

theorem TauCeti.NumberField.ncard_primesOverOfInertiaDeg_le {K : Type u_1} [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] {θ : NumberField.RingOfIntegers K} (hp : ¬p ∣ RingOfIntegers.exponent θ) (d : ℕ) : (primesOverOfInertiaDeg K p d).ncard ≤ {Q ∈ RingOfIntegers.monicFactorsMod θ p | Q.natDegree = d}.card

The Kummer–Dedekind counting bound. For a θ whose conductor exponent is prime to p, the primes of 𝓞 K above p with residue degree d are no more numerous than the degree-d monic irreducible factors of minpoly ℤ θ modulo p.

theorem TauCeti.NumberField.isCommonIndexDivisor_of_ncard_lt_ncard {K : Type u_1} [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] {d : ℕ} (hlt : (Polynomial.monicIrreduciblesOfDegree (ZMod p) d).ncard < (primesOverOfInertiaDeg K p d).ncard) : IsCommonIndexDivisor p K

The counting obstruction. If p has more primes of residue degree d than there are monic irreducible polynomials of degree d over 𝔽_p, then p divides the index of every integral primitive element.

Both counts are intrinsic to p, d and K: no bound is assumed, because the degree-d monic irreducibles over 𝔽_p are a fixed finite set independent of any generator.