English
Assume the same maximal and conductor hypotheses as above, with the minimal polynomial of x remaining integral modulo I. If this minimal polynomial mapped into the quotient is irreducible, then the mapped ideal I.map(algebraMap R S) is irreducible.
Русский
Пусть выполняются те же условия максимума и кондуктора; если минимальный неприводимый полином x в модульной системе сводится к неприводимому полиному в терминах модуля I, то образ I в S через алгебраическую карту является неприводимым.
LaTeX
$$(hI : IsMaximal I) (hI' : I ≠ ⊥) (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) (hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) : Irreducible (Ideal.map (algebraMap R S) I)$$
Lean4
theorem irreducible_map_of_irreducible_minpoly (hI : IsMaximal I) (hI' : I ≠ ⊥)
(hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x)
(hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) : Irreducible (I.map (algebraMap R S)) := by
classical
have mem_norm_factors :
normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) :=
by simp [normalizedFactors_irreducible hf]
suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = { y }
by
obtain ⟨y, hy⟩ := this
have h :=
prod_normalizedFactors
(show I.map (algebraMap R S) ≠ 0 by
rwa [← bot_eq_zero, Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
rw [← h]
exact irreducible_of_normalized_factor y (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])
rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']
use
((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩ :
Ideal S)
rw [Multiset.map_eq_singleton]
use ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩
refine ⟨?_, rfl⟩
apply Multiset.map_injective Subtype.coe_injective
rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
exact normalizedFactors_irreducible hf
