English
Let p be a polynomial over a T-algebra structure, and S, S' be commutative rings with an algebra map from T to each. If hp holds in the sense that p maps to zero in S' whenever it maps to zero in S, then every root of p over S is mapped by the algebra hom f: S →ₜ S' to a root of p.map(algebraMap T S') over S'. In particular, the root multiset of p over S is carried into the root multiset over S' via f.
Русский
Пусть p — многочлен над структурой T-алгебры, а S, S' — коммутативные кольца, сопряжённые с T; если выполняется условие hp: если p.map(algebraMap T S') = 0, тогда p.map(algebraMap T S) = 0, то любый корень p в S отображается алгебро-отображением f: S →ₜ S' в корень многочлена p.map(algebraMap T S') в S'. Иными словами, корневой набор p над S отображается в корневой набор над S' через f.
LaTeX
$$$ (p.rootSet S).MapsTo f (p.rootSet S') $$$
Lean4
theorem rootSet_maps_to' {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S']
[Algebra T S'] (hp : p.map (algebraMap T S') = 0 → p.map (algebraMap T S) = 0) (f : S →ₐ[T] S') :
(p.rootSet S).MapsTo f (p.rootSet S') := fun x hx =>
by
rw [mem_rootSet'] at hx ⊢
rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]
exact ⟨mt hp hx.1, rfl⟩
