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

Let K be a number field and θ an algebraic integer of K.

• 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 θ.

• NumberField.Ideal.primesOverSpanEquivMonicFactorsMod: The bijection between the prime ideals of K above p and the monic irreducible factors of minpoly ℤ θ modulo p for a prime p which doesn't divide the exponent of θ.

Main results

• NumberField.Ideal.primesOverSpanEquivMonicFactorsMod: The ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is spanned by p and Q(θ).

• NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply: The residual degree of the ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is equal to the degree of Q mod p.

• NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply: The ramification index of the ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is equal to the multiplicity of Q mod p in minpoly ℤ θ.

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.

Equations

• RingOfIntegers.exponent θ = Ideal.absNorm (Ideal.under ℤ (conductor ℤ θ))

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).

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• RingOfIntegers.monicFactorsMod θ p = (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))).toFinset

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(θ)).

Equations

• One or more equations did not get rendered due to their size.

def NumberField.Ideal.primesOverSpanEquivMonicFactorsMod {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) : ↑((Ideal.span {↑p}).primesOver (RingOfIntegers K)) ≃ { x : Polynomial (ZMod p) // x ∈ RingOfIntegers.monicFactorsMod θ p }

If p does not divide exponent θ, then the prime ideals above p in K are in bijection with the monic irreducible factors of minpoly ℤ θ modulo p.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)} (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p) : ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩) = ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk ⋯ ⋯ ⋯ ⋯).symm ⟨Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q, ⋯⟩)

theorem NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ} (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p) : ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = Ideal.span {↑p, (Polynomial.aeval θ) Q}

The ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is spanned by p and Q(θ).

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

theorem NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ} (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p) : (Ideal.span {↑p}).inertiaDeg ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree

The residual degree of the ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is equal to the degree of Q mod p.

theorem NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)} (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p) : (Ideal.span {↑p}).inertiaDeg ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩) = Q.natDegree

theorem NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ} (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p) : Ideal.ramificationIdx (algebraMap ℤ (RingOfIntegers K)) (Ideal.span {↑p}) ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

The ramification index of the ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is equal to the multiplicity of Q mod p in minpoly ℤ θ.

theorem NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply' {K : Type u_1} [Field K] {θ : RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] [NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)} (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p) : Ideal.ramificationIdx (algebraMap ℤ (RingOfIntegers K)) (Ideal.span {↑p}) ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩) = multiplicity Q (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))