Kummer–Dedekind: the primes over p, with their residue degrees and ramification indices

Let R be an integrally closed domain, let S be a Dedekind domain that is a torsion-free R-algebra, let x : S be integral over R, and let p be a nonzero maximal ideal of R that is prime to the conductor of R[x] in S. Mathlib's KummerDedekind file matches the prime factors of p S with the irreducible factors of minpoly R x modulo p, and matches their multiplicities. This file turns that match into the form ramification theory uses: a bijection

p.primesOver S ≃ {normalized irreducible factors of minpoly R x mod p}

under which the residue degree of a prime is the degree of the matching polynomial factor and its ramification index is the multiplicity of that factor. Together these say that the factorization of minpoly R x modulo p computes the splitting of p in S completely, which is the content of the Kummer–Dedekind criterion as it is used in practice.

The prime attached to a factor is explicit: it is span (p S ∪ {Q (x)}) for any lift Q of the factor, so the bijection can be evaluated on a concrete example.

Main definitions

• TauCeti.KummerDedekind.primesOverEquivNormalizedFactorsMinPolyMk: the bijection between the primes of S over p and the normalized irreducible factors of minpoly R x modulo p.
• TauCeti.KummerDedekind.quotientEquivQuotientSpan: the isomorphism (R ⧸ p)[X] ⧸ (Q) ≃+* S ⧸ span (p S ∪ {Q (x)}) for Q a lift of such a factor, which computes the residue field at the attached prime.

Main results

• TauCeti.KummerDedekind.primesOverEquivNormalizedFactorsMinPolyMk_symm_apply_coe: the prime attached to the class of Q is span (p S ∪ {Q (x)}).
• TauCeti.KummerDedekind.inertiaDeg_primesOverEquivNormalizedFactorsMinPolyMk_symm_apply: its residue degree is the degree of the factor.
• TauCeti.KummerDedekind.ramificationIdx_primesOverEquivNormalizedFactorsMinPolyMk_symm_apply: its ramification index is the multiplicity of the factor in minpoly R x modulo p.
• TauCeti.KummerDedekind.Ideal.irreducible_map_iff_irreducible_minpoly: p stays prime in S exactly when minpoly R x is irreducible modulo p.

Provenance

These are the arbitrary-Dedekind-domain form of Xavier Roblot's NumberField.Ideal.primesOverSpanEquivMonicFactorsMod, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply and NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply of Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean, and the proofs follow his, with the ℤ-to-ZMod p plumbing that his statements need dropped.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, Proposition 8.3.

noncomputable def TauCeti.KummerDedekind.primesOverEquivNormalizedFactorsMinPolyMk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hp0 : p ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) : ↑(p.primesOver S) ≃ ↑{d : Polynomial (R ⧸ p) | d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))}

The Kummer–Dedekind criterion: the primes of S lying over a nonzero maximal ideal p of R prime to the conductor of R[x] correspond to the normalized irreducible factors of minpoly R x modulo p.

Equations

• TauCeti.KummerDedekind.primesOverEquivNormalizedFactorsMinPolyMk hp hp0 hx hx' = (Set.equivOfEq ⋯).trans (KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hp hp0 hx hx')

theorem TauCeti.KummerDedekind.primesOverEquivNormalizedFactorsMinPolyMk_symm_apply_coe {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hp0 : p ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) {Q : Polynomial R} (hQ : Polynomial.map (Ideal.Quotient.mk p) Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))) : ↑((primesOverEquivNormalizedFactorsMinPolyMk hp hp0 hx hx').symm ⟨Polynomial.map (Ideal.Quotient.mk p) Q, hQ⟩) = Ideal.span (↑(Ideal.map (algebraMap R S) p) ∪ {(Polynomial.aeval x) Q})

The prime of S attached by TauCeti.KummerDedekind.primesOverEquivNormalizedFactorsMinPolyMk to the class modulo p of a lift Q is spanned by p S together with Q (x).

noncomputable def TauCeti.KummerDedekind.quotientEquivQuotientSpan {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) {Q : Polynomial R} (hQ : Polynomial.map (Ideal.Quotient.mk p) Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))) : Polynomial (R ⧸ p) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk p) Q} ≃+* S ⧸ Ideal.span (↑(Ideal.map (algebraMap R S) p) ∪ {(Polynomial.aeval x) Q})

The residue ring at a Kummer–Dedekind factor: for Q a lift of a normalized irreducible factor of minpoly R x modulo p, the quotient of S by the prime span (p S ∪ {Q (x)}) attached to that factor is (R ⧸ p)[X] modulo the factor.

Equations

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

@[simp]

theorem TauCeti.KummerDedekind.quotientEquivQuotientSpan_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) {Q : Polynomial R} (hQ : Polynomial.map (Ideal.Quotient.mk p) Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))) (P : Polynomial R) : (quotientEquivQuotientSpan hp hx hx' hQ) ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk p) Q})) (Polynomial.map (Ideal.Quotient.mk p) P)) = (Ideal.Quotient.mk (Ideal.span (↑(Ideal.map (algebraMap R S) p) ∪ {(Polynomial.aeval x) Q}))) ((Polynomial.aeval x) P)

TauCeti.KummerDedekind.quotientEquivQuotientSpan carries the class of a polynomial P over R ⧸ p to the class of P (x).

theorem TauCeti.KummerDedekind.inertiaDeg_primesOverEquivNormalizedFactorsMinPolyMk_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hp0 : p ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) {d : Polynomial (R ⧸ p)} (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))) : (↑((primesOverEquivNormalizedFactorsMinPolyMk hp hp0 hx hx').symm ⟨d, hd⟩)).inertiaDeg R = d.natDegree

The residue degree of a Kummer–Dedekind factor is the degree of the factor: the prime of S over p attached to a normalized irreducible factor d of minpoly R x modulo p has Ideal.inertiaDeg equal to d.natDegree.

theorem TauCeti.KummerDedekind.ramificationIdx_primesOverEquivNormalizedFactorsMinPolyMk_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hp0 : p ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) {d : Polynomial (R ⧸ p)} (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))) : (↑((primesOverEquivNormalizedFactorsMinPolyMk hp hp0 hx hx').symm ⟨d, hd⟩)).ramificationIdx R = multiplicity d (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))

The ramification index of a Kummer–Dedekind factor is its multiplicity: the prime of S over p attached to a normalized irreducible factor d of minpoly R x modulo p has Ideal.ramificationIdx equal to the multiplicity of d in minpoly R x modulo p.

theorem TauCeti.KummerDedekind.Ideal.irreducible_minpoly_of_irreducible_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) (h : Irreducible (Ideal.map (algebraMap R S) p)) : Irreducible (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))

The converse of Ideal.irreducible_map_of_irreducible_minpoly. If p S is irreducible, that is, if p stays prime in S, then minpoly R x modulo p is irreducible.

theorem TauCeti.KummerDedekind.Ideal.irreducible_map_iff_irreducible_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {p : Ideal R} (hp : p.IsMaximal) (hp0 : p ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤) (hx' : IsIntegral R x) : Irreducible (Ideal.map (algebraMap R S) p) ↔ Irreducible (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))

The Kummer–Dedekind irreducibility criterion. p stays prime in S exactly when minpoly R x is irreducible modulo p.