English
If f ∈ K[X] splits over id_K and is monic, and every root is in the range of algebraMap R K, then f is in Polynomial.lifts (algebraMap R K).
Русский
Если f ∈ K[X] распадается над id_K, моноичен, и каждый корень лежит в диапазоне algebraMap R K, то f принадлежит Polynomial.lifts (algebraMap R K).
LaTeX
$$$\\forall R,K,L,\\; [CommRing R]\\; [Field K]\\; [Field L]\\; f:\\ Polynomial K,\\; (\\text{Splits}(\\mathrm{id}_K,f)) \\land f.Monic \\land (\\forall a, a\\in f.\\text{roots} \\Rightarrow a \\in (\\mathrm{algebraMap } R K).range) \\Rightarrow f \\in Polynomial.lifts(\\mathrm{algebraMap } R K).$$$
Lean4
theorem mem_lift_of_splits_of_roots_mem_range [Algebra R K] {f : K[X]} (hs : f.Splits (RingHom.id K)) (hm : f.Monic)
(hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range) : f ∈ Polynomial.lifts (algebraMap R K) :=
by
rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_liftsRing]
refine Subring.multiset_prod_mem _ _ fun P hP => ?_
obtain ⟨b, hb, rfl⟩ := Multiset.mem_map.1 hP
exact Subring.sub_mem _ (X_mem_lifts _) (C'_mem_lifts (hr _ hb))
