# Kummer-Dedekind theorem #

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 #

• 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.

## TODO #

• Prove the Kummer-Dedekind theorem in full generality.

• Prove the converse of Ideal.irreducible_map_of_irreducible_minpoly.

• Prove that normalizedFactorsMapEquivNormalizedFactorsMinPolyMk can be expressed as normalizedFactorsMapEquivNormalizedFactorsMinPolyMk 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][Neukirch1992]

## Tags #

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

def conductor (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] (x : 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
• = { carrier := {a : S | ∀ (b : S), a * b Algebra.adjoin R {x}}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem conductor_eq_of_eq {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {y : S} (h : (Algebra.adjoin R {x}) = (Algebra.adjoin R {y})) :
=
theorem conductor_subset_adjoin {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} :
theorem mem_conductor_iff {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {y : S} :
y ∀ (b : S), y * b Algebra.adjoin R {x}
theorem conductor_eq_top_of_adjoin_eq_top {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} (h : Algebra.adjoin R {x} = ) :
theorem conductor_eq_top_of_powerBasis {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] (pb : ) :
conductor R pb.gen =
theorem mem_coeSubmodule_conductor {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {L : Type u_3} [] [Algebra S L] [Algebra R L] [] [] {x : S} {y : L} :
y ∀ (z : S), y * () z Algebra.adjoin R {() x}
theorem prod_mem_ideal_map_of_mem_conductor {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {I : } {p : R} {z : S} (hp : p Ideal.comap () ()) (hz' : z Ideal.map () I) :
() 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} [] [] [Algebra R S] {x : S} {I : } (hx : Ideal.comap () () I = ) (h_alg : Function.Injective (algebraMap ((Algebra.adjoin R {x})) S)) :

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} [] [] [Algebra R S] {x : S} {I : } (hx : Ideal.comap () () I = ) (h_alg : Function.Injective (algebraMap ((Algebra.adjoin R {x})) S)) :

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.
Instances For
@[simp]
theorem quotAdjoinEquivQuotMap_apply_mk {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {I : } (hx : Ideal.comap () () I = ) (h_alg : Function.Injective (algebraMap ((Algebra.adjoin R {x})) S)) (a : (Algebra.adjoin R {x})) :
noncomputable def KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {I : } [] [] [] (hI : I.IsMaximal) (hI' : I ) (hx : Ideal.comap () () I = ) (hx' : ) :
{J : | } {d : Polynomial (R I) | }

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
• One or more equations did not get rendered due to their size.
Instances For
theorem KummerDedekind.multiplicity_factors_map_eq_multiplicity {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {I : } [] [] [] (hI : I.IsMaximal) (hI' : I ) (hx : Ideal.comap () () I = ) (hx' : ) {J : } (hJ : ) :
multiplicity J (Ideal.map () I) = multiplicity (( J, hJ)) (Polynomial.map (minpoly R x))

The second half of the Kummer-Dedekind Theorem in the monogenic case, 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} [] [] [Algebra R S] {x : S} {I : } [] [] [] (hI : I.IsMaximal) (hI' : I ) (hx : Ideal.comap () () I = ) (hx' : ) :
= Multiset.map (fun (f : {d : Polynomial (R I) | }) => (.symm f)) .attach

The Kummer-Dedekind Theorem.

theorem KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {x : S} {I : } [] [] [] (hI : I.IsMaximal) (hI' : I ) (hx : Ideal.comap () () I = ) (hx' : ) (hf : Irreducible (Polynomial.map (minpoly R x))) :