Kummer-Dedekind theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the monogenic version of the Kummer-Dedekind theorem on the splitting of prime ideals in an extension of the ring of integers. This states that if I is a prime ideal of Dedekind domain R and S = R[α] for some α that is integral over R with minimal polynomial f, 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 #

normalized_factors_map_equiv_normalized_factors_min_poly_mk : 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 (algebra_map R S) is irreducible if (map I^.quotient.mk (minpoly R pb.gen)) is irreducible, where pb is a power basis of S over R.

TODO #

Prove the Kummer-Dedekind theorem in full generality.
Prove the converse of ideal.irreducible_map_of_irreducible_minpoly.
Prove that normalized_factors_map_equiv_normalized_factors_min_poly_mk can be expressed as normalized_factors_map_equiv_normalized_factors_min_poly_mk g = ⟨I, G(α)⟩ for g a prime factor of f mod I and G a lift of g to R[X].

References #

J. Neukirch, Algebraic Number Theory

Tags #

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

source

def conductor (R : Type u_1) {S : Type u_2} [comm_ring R] [comm_ring 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' := _}

source

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

conductor R x = conductor R y

source

theorem conductor_subset_adjoin {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} :

↑(conductor R x) ⊆ ↑(algebra.adjoin R {x})

source

theorem mem_conductor_iff {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x y : S} :

y ∈ conductor R x ↔ ∀ (b : S), y * b ∈ algebra.adjoin R {x}

source

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

conductor R x = ⊤

source

theorem conductor_eq_top_of_power_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) :

conductor R pb.gen = ⊤

source

theorem prod_mem_ideal_map_of_mem_conductor {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} {p : R} {z : S} (hp : p ∈ ideal.comap (algebra_map R S) (conductor R x)) (hz' : z ∈ ideal.map (algebra_map R S) I) :

⇑(algebra_map R S) p * z ∈ ⇑(algebra_map ↥(algebra.adjoin R {x}) S) '' ↑(ideal.map (algebra_map 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

source

theorem comap_map_eq_map_adjoin_of_coprime_conductor {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (h_alg : function.injective ⇑(algebra_map ↥(algebra.adjoin R {x}) S)) :

ideal.comap (algebra_map ↥(algebra.adjoin R {x}) S) (ideal.map (algebra_map R S) I) = ideal.map (algebra_map 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.

source

noncomputable def quot_adjoin_equiv_quot_map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (h_alg : function.injective ⇑(algebra_map ↥(algebra.adjoin R {x}) S)) :

↥(algebra.adjoin R {x}) ⧸ ideal.map (algebra_map R ↥(algebra.adjoin R {x})) I ≃+* S ⧸ ideal.map (algebra_map 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

quot_adjoin_equiv_quot_map hx h_alg = ring_equiv.of_bijective (ideal.quotient.lift (ideal.map (algebra_map R ↥(algebra.adjoin R {x})) I) ((ideal.quotient.mk (ideal.map (algebra_map R S) I)).comp (algebra_map ↥(algebra.adjoin R {x}) S)) quot_adjoin_equiv_quot_map._proof_1) _

source

@[simp]

theorem quot_adjoin_equiv_quot_map_apply_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (h_alg : function.injective ⇑(algebra_map ↥(algebra.adjoin R {x}) S)) (a : ↥(algebra.adjoin R {x})) :

⇑(quot_adjoin_equiv_quot_map hx h_alg) (⇑(ideal.quotient.mk (ideal.map (algebra_map R ↥(algebra.adjoin R {x})) I)) a) = ⇑(ideal.quotient.mk (ideal.map (algebra_map R S) I)) ↑a

source

noncomputable def kummer_dedekind.normalized_factors_map_equiv_normalized_factors_min_poly_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} [is_domain R] [is_integrally_closed R] [is_domain S] [is_dedekind_domain S] [no_zero_smul_divisors R S] (hI : I.is_maximal) (hI' : I ≠ ⊥) (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (hx' : is_integral R x) :

↥{J : ideal S | J ∈ unique_factorization_monoid.normalized_factors (ideal.map (algebra_map R S) I)} ≃ ↥{d : polynomial (R ⧸ I) | d ∈ unique_factorization_monoid.normalized_factors (polynomial.map (ideal.quotient.mk I) (minpoly R x))}

The first half of the Kummer-Dedekind Theorem in the monogenic case, 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

kummer_dedekind.normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx' = (normalized_factors_equiv_of_quot_equiv ((quot_adjoin_equiv_quot_map hx kummer_dedekind.normalized_factors_map_equiv_normalized_factors_min_poly_mk._proof_16).symm.trans (((algebra.adjoin.power_basis' hx').quotient_equiv_quotient_minpoly_map I).to_ring_equiv.trans (ideal.quot_equiv_of_eq _))) _ _).trans (normalized_factors_equiv_span_normalized_factors _).symm

source

theorem kummer_dedekind.multiplicity_factors_map_eq_multiplicity {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} [is_domain R] [is_integrally_closed R] [is_domain S] [is_dedekind_domain S] [no_zero_smul_divisors R S] (hI : I.is_maximal) (hI' : I ≠ ⊥) (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (hx' : is_integral R x) {J : ideal S} (hJ : J ∈ unique_factorization_monoid.normalized_factors (ideal.map (algebra_map R S) I)) :

multiplicity J (ideal.map (algebra_map R S) I) = multiplicity ↑(⇑(kummer_dedekind.normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx') ⟨J, hJ⟩) (polynomial.map (ideal.quotient.mk I) (minpoly R x))

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

source

theorem kummer_dedekind.normalized_factors_ideal_map_eq_normalized_factors_min_poly_mk_map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} [is_domain R] [is_integrally_closed R] [is_domain S] [is_dedekind_domain S] [no_zero_smul_divisors R S] (hI : I.is_maximal) (hI' : I ≠ ⊥) (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (hx' : is_integral R x) :

unique_factorization_monoid.normalized_factors (ideal.map (algebra_map R S) I) = multiset.map (λ (f : ↥{d : polynomial (R ⧸ I) | d ∈ unique_factorization_monoid.normalized_factors (polynomial.map (ideal.quotient.mk I) (minpoly R x))}), ↑(⇑((kummer_dedekind.normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx').symm) f)) (unique_factorization_monoid.normalized_factors (polynomial.map (ideal.quotient.mk I) (minpoly R x))).attach

The Kummer-Dedekind Theorem.

source

theorem kummer_dedekind.ideal.irreducible_map_of_irreducible_minpoly {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x : S} {I : ideal R} [is_domain R] [is_integrally_closed R] [is_domain S] [is_dedekind_domain S] [no_zero_smul_divisors R S] (hI : I.is_maximal) (hI' : I ≠ ⊥) (hx : ideal.comap (algebra_map R S) (conductor R x) ⊔ I = ⊤) (hx' : is_integral R x) (hf : irreducible (polynomial.map (ideal.quotient.mk I) (minpoly R x))) :

irreducible (ideal.map (algebra_map R S) I)