Prime counts and residue degrees by Kummer–Dedekind

Mathlib's number-field Kummer–Dedekind theorem (NumberField.Ideal.primesOverSpanEquivMonicFactorsMod) is a bijection between the primes of 𝓞 K above a rational prime p and the monic irreducible factors of minpoly ℤ θ modulo p, valid whenever p does not divide the conductor exponent of the algebraic integer θ. This file records both its cardinality form and its residue-degree form: the number of primes above p is the number of distinct factors, and their residue degrees are the factors' degrees. When the reduction is squarefree, its factor-degree multiset gives the splitting type directly. These forms are used to read splitting laws from a generator, for instance the quadratic laws of TauCeti.NumberTheory.NumberField.Quadratic.Splitting.

The first instance is the prime 2 for a generator ω with minimal polynomial X² - X + c and odd conductor exponent: the reduction X² + X + c mod 2 is X (X + 1) when c is even and the third cyclotomic polynomial X² + X + 1, irreducible over 𝔽₂, when c is odd, so there are two primes above 2 in the first case and one in the second. The conductor exponent of such a generator is automatically odd, since X² + X + c is separable over 𝔽₂.

Main results

• RingOfIntegers.ncard_primesOver_eq_card_monicFactorsMod: the number of primes of 𝓞 K above p equals the number of monic irreducible factors of minpoly ℤ θ mod p, for p ∤ exponent θ.
• RingOfIntegers.map_inertiaDeg_primesOver_eq_map_natDegree_monicFactorsMod: the multiset of residue degrees is the multiset of degrees of those distinct factors.
• RingOfIntegers.map_inertiaDeg_primesOver_eq_factorDegrees: when the reduction is squarefree, the same multiset is the factor-degree multiset with multiplicity.
• TauCeti.NumberField.inertiaDeg_eq_natDegree_primesOverSpanEquivMonicFactorsMod: the Kummer–Dedekind bijection preserves residue degree pointwise.
• NumberField.card_monicFactorsMod_two_of_minpoly_eq_X_sq_sub_X_add: the reduction mod 2 of X² - X + c has if 2 ∣ c then 2 else 1 monic irreducible factors.
• NumberField.ncard_primesOver_two_of_minpoly_eq_X_sq_sub_X_add: for a generator with minimal polynomial X² - X + c and odd conductor exponent, the number of primes above 2 is if 2 ∣ c then 2 else 1.
• NumberField.not_two_dvd_exponent_of_minpoly_eq_X_sq_sub_X_add: a generator of K with minimal polynomial X² - X + c has odd conductor exponent.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §8, Proposition (8.3).

theorem TauCeti.NumberField.inertiaDeg_eq_natDegree_primesOverSpanEquivMonicFactorsMod {K : Type u_1} [Field K] [NumberField K] {p : ℕ} [Fact (Nat.Prime p)] {θ : NumberField.RingOfIntegers K} (hp : ¬p ∣ RingOfIntegers.exponent θ) (Q : ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K))) : (↑Q).inertiaDeg ℤ = (↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp) Q)).natDegree

The Kummer–Dedekind bijection preserves degree. The residue degree of a prime above p equals the degree of its corresponding monic irreducible factor modulo p.

theorem RingOfIntegers.ncard_primesOver_eq_card_monicFactorsMod {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ exponent θ) : ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = (monicFactorsMod θ p).card

The Kummer–Dedekind count. When p does not divide the conductor exponent of θ, the primes of 𝓞 K above p are counted by the monic irreducible factors of minpoly ℤ θ mod p.

theorem RingOfIntegers.map_inertiaDeg_primesOver_eq_map_natDegree_monicFactorsMod {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ exponent θ) : Multiset.map (fun (Q : ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K))) => (↑Q).inertiaDeg ℤ) Finset.univ.val = Multiset.map Polynomial.natDegree (monicFactorsMod θ p).val

The residue degrees of the primes above p are the degrees of the distinct monic irreducible factors of the minimal polynomial modulo p, when Kummer–Dedekind applies.

theorem RingOfIntegers.map_inertiaDeg_primesOver_eq_factorDegrees {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ exponent θ) (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))) : Multiset.map (fun (Q : ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K))) => (↑Q).inertiaDeg ℤ) Finset.univ.val = (minpoly ℤ θ).factorDegrees p

At a prime where the reduction of minpoly ℤ θ is squarefree, the splitting type is its multiset of factor degrees. The conductor-exponent hypothesis permits the Kummer–Dedekind correspondence.

theorem NumberField.card_monicFactorsMod_two_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] {ω : RingOfIntegers K} {c : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C c) : (RingOfIntegers.monicFactorsMod ω 2).card = if 2 ∣ c then 2 else 1

The monic irreducible factors of X² - X + c modulo 2. For ω with minimal polynomial X² - X + c over ℤ, the reduction of that polynomial modulo 2 has two monic irreducible factors when c is even, since X² + X = X (X + 1) over 𝔽₂, and one when c is odd, since X² + X + 1 has no root in 𝔽₂.

theorem NumberField.not_two_dvd_exponent_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] [NumberField K] {ω : RingOfIntegers K} {c : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C c) (hgen : ℚ[↑ω] = ⊤) : ¬2 ∣ RingOfIntegers.exponent ω

A generator of K with minimal polynomial X² - X + c over ℤ has odd conductor exponent: its minimal polynomial is separable modulo 2.

theorem NumberField.ncard_primesOver_two_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] [NumberField K] {ω : RingOfIntegers K} {c : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C c) (hexp : ¬2 ∣ RingOfIntegers.exponent ω) : ((Ideal.span {2}).primesOver (RingOfIntegers K)).ncard = if 2 ∣ c then 2 else 1

The number of primes above 2 for a generator with minimal polynomial X² - X + c. Let K be generated over ℚ by an algebraic integer ω with minimal polynomial X² - X + c over ℤ, and suppose 2 does not divide the conductor exponent of ω. Then there are two primes of 𝓞 K above 2 when c is even and one when c is odd.