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 #

Main results #

TODO #

References #

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) :

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

Instances For
    theorem conductor_eq_of_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [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} [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 : S} {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} = ) :
    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 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 { x // x Algebra.adjoin R {x} } S) '' ↑(Ideal.map (algebraMap R { x // x Algebra.adjoin R {x} }) I)

    This technical lemma tell us that if C is the conductor of R and I is an ideal of R then p * (I * S) ⊆ I * R 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 { x // x Algebra.adjoin R {x} } S)) :
    Ideal.comap (algebraMap { x // x Algebra.adjoin R {x} } S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R { x // x Algebra.adjoin R {x} }) I

    A technical result telling us that (I * S) ∩ R = I * R 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 { x // x Algebra.adjoin R {x} } S)) :
    { x // x Algebra.adjoin R {x} } Ideal.map (algebraMap R { x // x Algebra.adjoin R {x} }) I ≃+* S Ideal.map (algebraMap R S) I

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

    Instances For
      @[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 { x // x Algebra.adjoin R {x} } S)) (a : { x // x Algebra.adjoin R {x} }) :
      ↑(quotAdjoinEquivQuotMap hx h_alg) (↑(Ideal.Quotient.mk (Ideal.map (algebraMap R { x // x Algebra.adjoin R {x} }) I)) a) = ↑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a

      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.

      Instances For

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