Kummer-Dedekind theorem

This file proves the Kummer-Dedekind theorem on the splitting of prime ideals in an extension of the ring of integers. This states the following: assume we are given

• A prime ideal I of Dedekind domain R
• An R-algebra S that is a Dedekind Domain
• An α : S such that that is integral over R with minimal polynomial f If the conductor 𝓒 of x is such that 𝓒 ∩ R is coprime to I then the prime factorisations of I * S and f mod I have the same shape, i.e. they have the same number of prime factors, and each prime factors of I * S can be paired with a prime factor of f mod I in a way that ensures multiplicities match (in fact, this pairing can be made explicit with a formula).

Main definitions

• normalizedFactorsMapEquivNormalizedFactorsMinPolyMk : The bijection in the Kummer-Dedekind theorem. This is the pairing between the prime factors of I * S and the prime factors of f mod I.

Main results

• normalized_factors_ideal_map_eq_normalized_factors_min_poly_mk_map : The Kummer-Dedekind theorem.
• Ideal.irreducible_map_of_irreducible_minpoly : I.map (algebraMap R S) is irreducible if (map (Ideal.Quotient.mk I) (minpoly R pb.gen)) is irreducible, where pb is a power basis of S over R.
  • normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span : Let Q be a lift of factor of the minimal polynomial of x, a generator of S over R, taken mod I. Then (the reduction of) Q corresponds via normalizedFactorsMapEquivNormalizedFactorsMinPolyMk to span (I.map (algebraMap R S) ∪ {Q.aeval x}).

TODO

• Prove the converse of Ideal.irreducible_map_of_irreducible_minpoly.

References

• J. Neukirch, Algebraic Number Theory

Tags

kummer, dedekind, kummer dedekind, dedekind-kummer, dedekind kummer

def conductor (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) : Ideal S

Let S / R be a ring extension and x : S, then the conductor of R<x> is the biggest ideal of S contained in R<x>.

Equations

• conductor R x = { carrier := {a : S | ∀ (b : S), a * b ∈ Algebra.adjoin R {x}}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem conductor_eq_of_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x y : S} (h : ↑(Algebra.adjoin R {x}) = ↑(Algebra.adjoin R {y})) : conductor R x = conductor R y

theorem conductor_subset_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : ↑(conductor R x) ⊆ ↑(Algebra.adjoin R {x})

theorem mem_conductor_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x y : S} : y ∈ conductor R x ↔ ∀ (b : S), y * b ∈ Algebra.adjoin R {x}

theorem conductor_eq_top_of_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : Algebra.adjoin R {x} = ⊤) : conductor R x = ⊤

theorem conductor_eq_top_of_powerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) : conductor R pb.gen = ⊤

theorem adjoin_eq_top_of_conductor_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : conductor R x = ⊤) : Algebra.adjoin R {x} = ⊤

theorem conductor_eq_top_iff_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : conductor R x = ⊤ ↔ Algebra.adjoin R {x} = ⊤

theorem mem_coeSubmodule_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {L : Type u_3} [CommRing L] [Algebra S L] [Algebra R L] [IsScalarTower R S L] [NoZeroSMulDivisors S L] {x : S} {y : L} : y ∈ IsLocalization.coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ Algebra.adjoin R {(algebraMap S L) x}

theorem prod_mem_ideal_map_of_mem_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} {p : R} {z : S} (hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x)) (hz' : z ∈ Ideal.map (algebraMap R S) I) : (algebraMap R S) p * z ∈ ⇑(algebraMap (↥(Algebra.adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)

This technical lemma tell us that if C is the conductor of R<x> and I is an ideal of R then p * (I * S) ⊆ I * R<x> for any p in C ∩ R

theorem comap_map_eq_map_adjoin_of_coprime_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)) : Ideal.comap (algebraMap (↥(Algebra.adjoin R {x})) S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I

A technical result telling us that (I * S) ∩ R<x> = I * R<x> for any ideal I of R.

noncomputable def quotAdjoinEquivQuotMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)) : ↥(Algebra.adjoin R {x}) ⧸ Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I ≃+* S ⧸ Ideal.map (algebraMap R S) I

The canonical morphism of rings from R<x> ⧸ (I*R<x>) to S ⧸ (I*S) is an isomorphism when I and (conductor R x) ∩ R are coprime.

Equations

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

@[simp]

theorem quotAdjoinEquivQuotMap_apply_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)) (a : ↥(Algebra.adjoin R {x})) : (quotAdjoinEquivQuotMap hx h_alg) ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)) a) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ↑a

noncomputable def KummerDedekind.quotMapEquivQuotQuotMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : S ⧸ Ideal.map (algebraMap R S) I ≃+* Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}

The isomorphism of rings between S / I and (R / I)[X] / minpoly x when I and (conductor R x) ∩ R are coprime.

Equations

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

theorem KummerDedekind.quotMapEquivQuotQuotMap_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) (Q : Polynomial R) : (quotMapEquivQuotQuotMap hx hx').symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) (Polynomial.map (Ideal.Quotient.mk I) Q)) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval x) Q)

noncomputable def KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : ↑{J : Ideal S | J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)} ≃ ↑{d : Polynomial (R ⧸ I) | d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}

The first half of the Kummer-Dedekind Theorem, stating that the prime factors of I*S are in bijection with those of the minimal polynomial of the generator of S over R, taken mod I.

Equations

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

theorem KummerDedekind.emultiplicity_factors_map_eq_emultiplicity {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) {J : Ideal S} (hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)) : emultiplicity J (Ideal.map (algebraMap R S) I) = emultiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

The second half of the Kummer-Dedekind Theorem, stating that the bijection FactorsEquiv' defined in the first half preserves multiplicities.

theorem KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I) = Multiset.map (fun (f : ↑{d : Polynomial (R ⧸ I) | d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}) => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

The Kummer-Dedekind Theorem.

theorem KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) (hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) : Irreducible (Ideal.map (algebraMap R S) I)

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

Let Q be a lift of factor of the minimal polynomial of x, a generator of S over R, taken mod I. Then (the reduction of) Q corresponds via normalizedFactorsMapEquivNormalizedFactorsMinPolyMk to span (I.map (algebraMap R S) ∪ {Q.aeval x}).