Kummer-Dedekind criterion for the splitting of prime numbers

In this file, we give a specialized version of the Kummer-Dedekind criterion for the case of the splitting of rational primes in number fields.

Main definitions

• RingOfIntegers.exponent: the smallest positive integer d contained in the conductor of θ. It is the smallest integer such that d • 𝓞 K ⊆ ℤ[θ], see RingOfIntegers.exponent_eq_sInf.

• RingOfIntegers.ZModXQuotSpanEquivQuotSpan: The isomorphism between (ℤ / pℤ)[X] / (minpoly θ) and 𝓞 K / p(𝓞 K) for a prime p which doesn't divide the exponent of θ.

def RingOfIntegers.exponent {K : Type u_1} [Field K] (θ : NumberField.RingOfIntegers K) : ℕ

The smallest positive integer d contained in the conductor of θ. It is the smallest integer such that d • 𝓞 K ⊆ ℤ[θ], see exponent_eq_sInf. It is set to 0 if d does not exists.

theorem RingOfIntegers.exponent_eq_one_iff {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} : exponent θ = 1 ↔ Algebra.adjoin ℤ {θ} = ⊤

theorem RingOfIntegers.not_dvd_exponent_iff {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] : ¬p ∣ exponent θ ↔ Codisjoint (Ideal.comap (algebraMap ℤ (NumberField.RingOfIntegers K)) (conductor ℤ θ)) (Ideal.span {↑p})

theorem RingOfIntegers.exponent_eq_sInf {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} : exponent θ = sInf {d : ℕ | 0 < d ∧ ↑d ∈ conductor ℤ θ}

def RingOfIntegers.ZModXQuotSpanEquivQuotSpan {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ exponent θ) : Polynomial (ZMod p) ⧸ Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ≃+* NumberField.RingOfIntegers K ⧸ Ideal.span {↑p}

If p doesn't divide the exponent of θ, then (ℤ / pℤ)[X] / (minpoly θ) ≃+* 𝓞 K / p(𝓞 K).

theorem RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ exponent θ) (Q : Polynomial ℤ) : (ZModXQuotSpanEquivQuotSpan hp) ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)})) (Polynomial.map (Int.castRingHom (ZMod p)) Q)) = (Ideal.Quotient.mk (Ideal.span {↑p})) ((Polynomial.aeval θ) Q)

@[reducible, inline]

abbrev RingOfIntegers.monicFactorsMod {K : Type u_1} [Field K] (θ : NumberField.RingOfIntegers K) (p : ℕ) [Fact (Nat.Prime p)] : Finset (Polynomial (ZMod p))

The finite set of monic irreducible factors of minpoly ℤ θ modulo p.

def RingOfIntegers.ZModXQuotSpanEquivQuotSpanPair {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ exponent θ) {Q : Polynomial ℤ} (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p) : Polynomial (ZMod p) ⧸ Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) Q} ≃+* NumberField.RingOfIntegers K ⧸ Ideal.span {↑p, (Polynomial.aeval θ) Q}

If p does not divide exponent θ and Q is a lift of a monic irreducible factor of minpoly ℤ θ modulo p, then (ℤ / pℤ)[X] / Q ≃+* 𝓞 K / (p, Q(θ)).