Theorems · Definition · number theory

KummerDedekind.quotMapEquivQuotQuotMap

{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] →
                  [IsDedekindDomain S] →
                    [Module.IsTorsionFree R S] →
                      Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
                        IsIntegral R x →
                          S ⧸ Ideal.map (algebraMap R S) I ≃+*
                            Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}

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

Defined in

Mathlib.NumberTheory.KummerDedekind

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsIntegrallyClosedIsDedekindDomainModule.IsTorsionFree