Prime-norm ideals and residue roots

At primes coprime to the conductor exponent, residue roots account for all ideals of prime norm, not merely a subset of them.

theorem NairTenenbaum.conductor_exponent_mem {K : Type u_1} [Field K] (θ : NumberField.RingOfIntegers K) : ↑(RingOfIntegers.exponent θ) ∈ conductor ℤ θ

theorem NairTenenbaum.zmod_hom_ext_generator {K : Type u_1} [Field K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : Nat.Prime p) (hc : p.Coprime (RingOfIntegers.exponent θ)) {f g : NumberField.RingOfIntegers K →+* ZMod p} (hθ : f θ = g θ) : f = g

noncomputable def NairTenenbaum.primeNormIdealHom {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (I : { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = p }) : NumberField.RingOfIntegers K →+* ZMod p

The residue homomorphism attached to an ideal of prime absolute norm.

Equations

• NairTenenbaum.primeNormIdealHom hp I = (ZMod.ringEquivOfPrime (NumberField.RingOfIntegers K ⧸ ↑I) hp ⋯).symm.toRingHom.comp (Ideal.Quotient.mk ↑I)

theorem NairTenenbaum.primeNormIdealHom_ker {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (I : { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = p }) : RingHom.ker (primeNormIdealHom hp I) = ↑I

noncomputable def NairTenenbaum.primeNormIdealRoot {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : Nat.Prime p) (I : { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = p }) : ResidueRoots (minpoly ℤ θ) p

The polynomial root associated with a prime-norm ideal.

Equations

• NairTenenbaum.primeNormIdealRoot θ hp I = ⟨(NairTenenbaum.primeNormIdealHom hp I) θ, ⋯⟩

theorem NairTenenbaum.primeNormIdealRoot_injective {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : Nat.Prime p) (hc : p.Coprime (RingOfIntegers.exponent θ)) : Function.Injective (primeNormIdealRoot θ hp)

theorem NairTenenbaum.rootCount_minpoly_eq_idealNormCount {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : Nat.Prime p) (hc : p.Coprime (RingOfIntegers.exponent θ)) : rootCount (minpoly ℤ θ) p = idealNormCount K p