# Documentation

Mathlib.NumberTheory.KummerDedekind

# 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].

• [J. Neukirch, Algebraic Number Theory][Neukirch1992]

## Tags #

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