Theorems · Definition · number theory

KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {x : S} →
            {I : Ideal R} →
              [IsDomain R] →
                [IsIntegrallyClosed R] →
                  [inst_5 : IsDedekindDomain S] →
                    [Module.IsTorsionFree R S] →
                      (hI : I.IsMaximal) →
                        I ≠ ⊥ →
                          Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
                            IsIntegral R x →
                              ↑{J | J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)} ≃
                                ↑{d |
                                    d ∈
                                      UniqueFactorizationMonoid.normalizedFactors
                                        (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}

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.

Defined in

Mathlib.NumberTheory.KummerDedekind

Cited by

8 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIsDomainIsIntegrallyClosedIsDedekindDomainModule.IsTorsionFree