English
The equality emultiplicity stated for J in the previous theorem holds in the symmetric form with the image under the normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.
Русский
Справедливость кратностей J во втором виде теоремы аналогична первому виду через образ под нормализацией эквивалентности факторов.
LaTeX
$$$$ emultiplicity(J, I.map(\mathrm{algebraMap} R S)) = emultiplicity(\text{image under } \text{normalizedFactorsMapEquivNormalizedFactorsMinPolyMk} \langle J, hJ \rangle, \mathrm{map}(\minpoly R x)) $$$$
Lean4
/-- The second half of the **Kummer-Dedekind Theorem**, stating that the
bijection `FactorsEquiv'` defined in the first half preserves multiplicities. -/
theorem emultiplicity_factors_map_eq_emultiplicity (hI : IsMaximal I) (hI' : I ≠ ⊥)
(hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) {J : Ideal S}
(hJ : J ∈ normalizedFactors (I.map (algebraMap R S))) :
emultiplicity J (I.map (algebraMap R S)) =
emultiplicity (↑(normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' ⟨J, hJ⟩))
(Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) :=
by
rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Equiv.coe_trans, Function.comp_apply,
emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity,
normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity]
