English
Let R ⊆ K and L be algebras, p ∈ R[X], Splits algebraMap R K p. For any algebra hom f: K → Algebra, the image of p.rootSet K under f equals p.rootSet L.
Русский
Пусть R ⊆ K и L являются алгебрами, p ∈ R[X], распадается над алгебраMap R K. Для любого алгебра-гомоморфа f: K → L выполняется изображение множества корней p.rootSet_K равняется p.rootSet_L.
LaTeX
$$$\\forall R,K,L,\\; p:\\ Polynomial R,\\; (p.Splits(\\mathrm{algebraMap} R K))\\Rightarrow \\forall f:\\ K \\to_{R} L,\\; f '' p.\\text{rootSet }K = p.\\text{rootSet }L.$$$
Lean4
theorem image_rootSet [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) :
f '' p.rootSet K = p.rootSet L := by
classical
rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom, ←
roots_map _ ((splits_id_iff_splits (algebraMap R K)).mpr h), map_map, f.comp_algebraMap, ← rootSet]
