Documentation

Mathlib.NumberTheory.KummerDedekind

Kummer-Dedekind theorem #

This file proves the Kummer-Dedekind theorem on the splitting of prime ideals in an extension of the ring of integers. This states the following: assume we are given

Main definitions #

Main results #

TODO #

References #

Tags #

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

The isomorphism of rings between S / I and (R / I)[X] / minpoly x when I and (conductor R x) ∩ R are coprime.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

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

      Let Q be a lift of factor of the minimal polynomial of x, a generator of S over R, taken mod I. Then (the reduction of) Q corresponds via normalizedFactorsMapEquivNormalizedFactorsMinPolyMk to span (I.map (algebraMap R S) ∪ {Q.aeval x}).