Residue roots give ideals of prime norm

For a modulus coprime to the conductor exponent, Kummer–Dedekind identifies the quotient of the ring of integers with the quotient by the reduced minimal polynomial. Evaluation at a residue root gives an ideal of that norm; at a prime modulus this ideal is maximal.

noncomputable def NairTenenbaum.residueRootHom {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) (a : ResidueRoots (minpoly ℤ θ) p) : NumberField.RingOfIntegers K →+* ZMod p

The residue-algebra homomorphism induced by a polynomial root.

Equations

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

@[simp]

theorem NairTenenbaum.residueRootHom_apply_generator {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) (a : ResidueRoots (minpoly ℤ θ) p) : (residueRootHom θ hp a) θ = ↑a

theorem NairTenenbaum.residueRootHom_injective {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) : Function.Injective (residueRootHom θ hp)

noncomputable def NairTenenbaum.residueRootIdeal {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) (a : ResidueRoots (minpoly ℤ θ) p) : Ideal (NumberField.RingOfIntegers K)

The ideal obtained as the kernel of the residue-root homomorphism.

Equations

• NairTenenbaum.residueRootIdeal θ hp a = RingHom.ker (NairTenenbaum.residueRootHom θ hp a)

@[simp]

theorem NairTenenbaum.residueRootIdeal_absNorm {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) (a : ResidueRoots (minpoly ℤ θ) p) : Ideal.absNorm (residueRootIdeal θ hp a) = p

theorem NairTenenbaum.residueRootIdeal_injective {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) : Function.Injective (residueRootIdeal θ hp)

theorem NairTenenbaum.rootCount_minpoly_le_card_ideals_norm {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {p : ℕ} (hp : p.Coprime (RingOfIntegers.exponent θ)) : rootCount (minpoly ℤ θ) p ≤ Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = p }