English
For maximal I, and under appropriate nondegeneracy, the emultiplicity of J in I.map equals the emultiplicity of the corresponding image under the normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.
Русский
При максимальности I и при условии ненулевой общей степени, мультипликативная кратность J сохраняется под отображением в нормализованных множествах факторов.
LaTeX
$$$$ emultiplicity(J, I.map(\mathrm{algebraMap} R S)) = emultiplicity(\text{image under } \text{normalizedFactorsMapEquivNormalizedFactorsMinPolyMk}, J). $$$$
Lean4
/-- 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`. -/
noncomputable def normalizedFactorsMapEquivNormalizedFactorsMinPolyMk (hI : IsMaximal I) (hI' : I ≠ ⊥)
(hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
{J : Ideal S | J ∈ normalizedFactors (I.map (algebraMap R S))} ≃
{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :=
by
refine (normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx') ?_ ?_).trans ?_
· rwa [Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S), ← Ne]
· by_contra h
exact
(show Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0 from
Polynomial.map_monic_ne_zero (minpoly.monic hx'))
(span_singleton_eq_bot.mp h)
· refine (normalizedFactorsEquivSpanNormalizedFactors ?_).symm
exact Polynomial.map_monic_ne_zero (minpoly.monic hx')
