English
Let x be in an extension S of R, f a monic polynomial in R[X], and f weakly Eisenstein at a prime p. Then there exists y in the adjoin of x such that (a_p) y = x^{deg f}, where a_p is the image of p in S.
Русский
Пусть x принадлежит расширению S над R, f — моноик полином R[X], и f слабый Эйзенштейн на простом p. Существует элемент y в приумножаемом аджойнe x такой, что a_p y = x^{deg f}.
LaTeX
$$∃ y ∈ adjoin R ({ x } ), (algebraMap R S) p * y = x ^ (f.map (algebraMap R S)).natDegree$$
Lean4
theorem exists_mem_adjoin_mul_eq_pow_natDegree {x : S} (hx : aeval x f = 0) (hmo : f.Monic)
(hf : f.IsWeaklyEisensteinAt (Submodule.span R { p })) :
∃ y ∈ adjoin R ({ x } : Set S), (algebraMap R S) p * y = x ^ (f.map (algebraMap R S)).natDegree :=
by
rw [aeval_def, Polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one, sum_insert notMem_range_self,
sum_range, (hmo.map (algebraMap R S)).coeff_natDegree, one_mul] at hx
replace hx := eq_neg_of_add_eq_zero_left hx
have : ∀ n < f.natDegree, p ∣ f.coeff n := by
intro n hn
exact mem_span_singleton.1 (by simpa using hf.mem hn)
choose! φ hφ using this
conv_rhs at hx =>
congr
congr
· skip
ext i
rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le), RingHom.map_mul, mul_assoc]
rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]
refine ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩
exact
Subalgebra.mul_mem _ (Subalgebra.neg_mem _ (Subalgebra.one_mem _))
(Subalgebra.sum_mem _ fun i _ =>
Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
(Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _))
