English
Let f be a polynomial over R[X], and S a ring with a map from R to S. If f is weakly Eisenstein at P and hx = aeval x f = 0 in S with f monic, then for all i, the natDegree of f mapped to S is ≤ i implies x^i lies in the image of P, i.e., in P.map (algebraMap R S).
Русский
Пусть f — полином над R[X], S — кольцо с отображением из R в S. Если f является слабым Эйзенштейном относительно P и hx = aeval x f = 0 в S при некотором x, а f моничен, тогда для любого i выполняется: natDegree(f.map(алгебраMap R S)) ≤ i ⇒ x^i лежит в образе P в S.
LaTeX
$$$\\forall {R} [\\mathrm{CommRing}\,R] {f:R[X]} {S} [\\mathrm{CommRing}\,S] [\\mathrm{Algebra}\,R\,S] {\\mathcal P} : \\ f.IsWeaklyEisensteinAt\\mathcal P \\to ∀ {x:S}, aeval\\ x\\ f = 0 \\to f.Monic \\to ∀ i, (f.map (algebraMap R S)).natDegree ≤ i \\to x^i ∈ \\mathcal P.map (algebraMap R S)$$$
Lean4
theorem pow_natDegree_le_of_aeval_zero_of_monic_mem_map (hf : f.IsWeaklyEisensteinAt 𝓟) {x : S} (hx : aeval x f = 0)
(hmo : f.Monic) : ∀ i, (f.map (algebraMap R S)).natDegree ≤ i → x ^ i ∈ 𝓟.map (algebraMap R S) :=
by
suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S)
by
intro i hi
obtain ⟨k, hk⟩ := exists_add_of_le hi
rw [hk, pow_add]
exact mul_mem_right _ _ this
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx
exact pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
