Theorems · Theorem · number theory

KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span

∀ {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}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hI : I.IsMaximal) {Q : Polynomial R}
  (hQ :
    Polynomial.map (Ideal.Quotient.mk I) Q ∈
      UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
  (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x),
  ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩) =
    Ideal.span (↑(Ideal.map (algebraMap R S) I) ∪ {(Polynomial.aeval x) Q})

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}).

Defined in

Mathlib.NumberTheory.KummerDedekind

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsIntegrallyClosedIsDedekindDomainModule.IsTorsionFree