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
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
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 * Sand the prime factors of
f mod I.
Main results #
normalized_factors_ideal_map_eq_normalized_factors_min_poly_mk_map: The Kummer-Dedekind theorem.
I.map (algebraMap R S)is irreducible if
(map (Ideal.Quotient.mk I) (minpoly R pb.gen))is irreducible, where
pbis a power basis of
Prove the Kummer-Dedekind theorem in full generality.
Prove the converse of
normalizedFactorsMapEquivNormalizedFactorsMinPolyMkcan be expressed as
normalizedFactorsMapEquivNormalizedFactorsMinPolyMk g = ⟨I, G(α)⟩for
ga prime factor of
f mod Iand
Ga lift of
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]
kummer, dedekind, kummer dedekind, dedekind-kummer, dedekind kummer
This technical lemma tell us that if
C is the conductor of
I is an ideal of
p * (I * S) ⊆ I * R for any
C ∩ R
A technical result telling us that
(I * S) ∩ R for any ideal
The canonical morphism of rings from
S ⧸ (I*S) is an isomorphism
(conductor R x) ∩ R are coprime.
The first half of the Kummer-Dedekind Theorem in the monogenic case, stating that the prime
I*S are in bijection with those of the minimal polynomial of the generator of
The second half of the Kummer-Dedekind Theorem in the monogenic case, stating that the
FactorsEquiv' defined in the first half preserves multiplicities.
The Kummer-Dedekind Theorem.