normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map

English

Let I be a maximal ideal of R with I ≠ ⊥, and x ∈ S subject to integrality and conductor hypotheses. Then the multiset of normalized factors of the ideal I mapped into S equals the image under a natural equivalence of the normalized factors of the polynomial minpoly_R(x) after applying the quotient by I; in symbols, these two factorizations correspond under the canonical factor-map.

Русский

Пусть I является максимальной идеалом кольца R, I ≠ ⊥, и пусть x ∈ S удовлетворяет условиям интегрируемости и кондуктора. Тогда множество нормализованных факторов модуля I на S совпадает с образцом через естественное сопоставление нормализованных факторов минимального многочлена minpoly_R(x) после применения конечной факторизации: факторизации совпадают через соответствующее отображение.

LaTeX

$$$\operatorname{normalizedFactors}\left(I.map(\alpha)\right) = \operatorname{Multiset}.map\left( (\mathrm{normalizedFactorsMapEquivNormalizedFactorsMinPolyMk}~hI~hI'~hx~hx')^{-1} \;\cdot\; \right) \left( \operatorname{normalizedFactors}\left( Polynomial.map(Ideal.Quotient.mk I)\left(\minpoly R x\right) \right)\right).attach$$$

Lean4

/-- The **Kummer-Dedekind Theorem**. -/
theorem normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map (hI : IsMaximal I) (hI' : I ≠ ⊥)
    (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
    normalizedFactors (I.map (algebraMap R S)) =
      Multiset.map (fun f => ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f : Ideal S))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach :=
  by
  ext J
  by_cases hJ : J ∈ normalizedFactors (I.map (algebraMap R S))
  swap
  · rw [Multiset.count_eq_zero.mpr hJ, eq_comm, Multiset.count_eq_zero, Multiset.mem_map]
    simp only [not_exists]
    rintro J' ⟨_, rfl⟩
    exact hJ ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J').prop
  have := emultiplicity_factors_map_eq_emultiplicity hI hI' hx hx' hJ
  rw [emultiplicity_eq_count_normalizedFactors, emultiplicity_eq_count_normalizedFactors,
    UniqueFactorizationMonoid.normalize_normalized_factor _ hJ, UniqueFactorizationMonoid.normalize_normalized_factor,
    Nat.cast_inj] at this
  · refine
      this.trans
        ?_
          -- Get rid of the `map` by applying the equiv to both sides.

    generalize hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
    have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) = J := by
      rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk]
    subst this
    rw [Multiset.count_map_eq_count' fun f =>
        ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f : Ideal S),
      Multiset.count_attach]
    · exact Subtype.coe_injective.comp (Equiv.injective _)
  · exact (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop
  · exact irreducible_of_normalized_factor _ (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop
  · exact Polynomial.map_monic_ne_zero (minpoly.monic hx')
  · exact irreducible_of_normalized_factor _ hJ
  · rwa [← bot_eq_zero, Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]

Похожие утверждения