The conductor comparison for arbitrary coprime moduli

The quotient comparison used by Kummer–Dedekind works for every modulus coprime to the conductor exponent, not only for prime moduli.

theorem NairTenenbaum.conductor_sup_span_eq_top {K : Type u_1} [Field K] (θ : NumberField.RingOfIntegers K) {n : ℕ} (hn : n.Coprime (RingOfIntegers.exponent θ)) : Ideal.comap (algebraMap ℤ (NumberField.RingOfIntegers K)) (conductor ℤ θ) ⊔ Ideal.span {↑n} = ⊤

noncomputable def NairTenenbaum.residuePolynomialQuotientEquiv {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {n : ℕ} (hn : n.Coprime (RingOfIntegers.exponent θ)) : Polynomial (ZMod n) ⧸ Ideal.span {Polynomial.map (Int.castRingHom (ZMod n)) (minpoly ℤ θ)} ≃+* NumberField.RingOfIntegers K ⧸ Ideal.span {↑n}

The equivalence between the polynomial quotient and the residue algebra.

Equations

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

theorem NairTenenbaum.residuePolynomialQuotientEquiv_mk {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) {n : ℕ} (hn : n.Coprime (RingOfIntegers.exponent θ)) (Q : Polynomial ℤ) : (residuePolynomialQuotientEquiv θ hn) ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Int.castRingHom (ZMod n)) (minpoly ℤ θ)})) (Polynomial.map (Int.castRingHom (ZMod n)) Q)) = (Ideal.Quotient.mk (Ideal.span {↑n})) ((Polynomial.aeval θ) Q)