Dedekind's criterion #
Let θ be an integral primitive element of a number field K, with minimal polynomial
f = minpoly ℤ θ, and let p be a prime. Factor the reduction of f modulo p as
f mod p = ∏ i, φ i ^ e i,
with the φ i distinct monic irreducible polynomials over ZMod p and every e i > 0. Choose
lifts Φ i : ℤ[X] of the φ i. Then f - ∏ i, Φ i ^ e i reduces to zero modulo p, so it is
p H for an integer polynomial H (exists_C_mul_eq_minpoly_sub_prod). Dedekind's
criterion (not_dvd_index_iff) states that
p ∤ [𝓞 K : ℤ[θ]] ↔ ∀ i, e i = 1 ∨ ¬ φ i ∣ (H mod p).
The criterion decides, from f, p, the factorisation of f mod p and any choice of lifts,
whether p divides the index of the order ℤ[θ] in 𝓞 K, that is, whether ℤ[θ] is
p-maximal; in particular it makes the hypothesis of the Kummer–Dedekind theorem at p
checkable. Its truth value does not depend on which lifts Φ i, and hence which H, are chosen
(forall_eq_one_or_not_dvd_map_iff).
Main results #
TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_iff: Dedekind's criterion.TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_forall_eq_one_or_not_dvd_map,TauCeti.NumberField.IntegralPrimitiveElement.dvd_index_of_ne_one_of_dvd_map: its sufficient and its necessary direction.TauCeti.NumberField.IntegralPrimitiveElement.forall_eq_one_or_not_dvd_map_iff: the criterion does not depend on the lifts.TauCeti.NumberField.IntegralPrimitiveElement.exists_notMem_mul_mem_adjoin: the element ofℤ[θ]outside a prime abovepthat carries the sufficient direction.TauCeti.NumberField.IntegralPrimitiveElement.exists_aeval_eq_of_mem_adjoin_of_mem: an element ofℤ[θ]lying in a prime abovepcontainingΦ(θ)isΦ(θ) Q(θ) + p D(θ).
References #
- H. Cohen, A Course in Computational Algebraic Number Theory, Theorem 6.1.4.
The minimal polynomial differs from the product of the lifts by a multiple of p. If
minpoly ℤ θ reduces to ∏ i, φ i ^ e i modulo p and each Φ i lifts φ i, then
minpoly ℤ θ - ∏ i, Φ i ^ e i is p times an integer polynomial H.
Conversely, p H = minpoly ℤ θ - ∏ i, Φ i ^ e i recovers the factorisation of
minpoly ℤ θ modulo p from the lifts.
Evaluating C p * H = minpoly ℤ θ - ∏ i, Φ i ^ e i at θ.
An element of ℤ[θ] lying in a proper ideal P of 𝓞 K that contains p and Φ(θ),
where Φ reduces modulo p to an irreducible polynomial, is Φ(θ) Q(θ) + p D(θ) for integer
polynomials Q, D.
The key step of Dedekind's criterion. Let P be a prime of 𝓞 K containing p and
Φ i (θ). If e i = 1, or if φ i does not divide the reduction of H, then there is
σ ∈ ℤ[θ] outside P such that σ z ∈ ℤ[θ] whenever p z ∈ ℤ[θ].
Dedekind's criterion, the sufficient direction. If for every i either e i = 1 or
φ i does not divide the reduction of H, then p does not divide the index [𝓞 K : ℤ[θ]].
Dedekind's criterion, the necessary direction. If e i ≥ 2 and φ i divides the
reduction of H for some i, then p divides the index [𝓞 K : ℤ[θ]].
Dedekind's criterion. Let θ be an integral primitive element of K with minimal
polynomial f = minpoly ℤ θ, let p be a prime, and factor f mod p = ∏ i, φ i ^ e i into
distinct monic irreducible polynomials φ i over ZMod p, each with multiplicity e i > 0.
Choose lifts Φ i : ℤ[X] of the φ i and let H : ℤ[X] satisfy p H = f - ∏ i, Φ i ^ e i
(which records the factorisation, by map_minpoly_eq_prod_of_C_mul_eq). Then p does not
divide the index [𝓞 K : ℤ[θ]] if and only if, for every i, either e i = 1 or φ i does
not divide H mod p.
The right-hand side of Dedekind's criterion does not depend on the choice of the lifts
Φ i of the φ i, nor on the resulting H.