English
For polynomial p ∈ R[X] that splits over K, for any algebra hom f: K → L, the adjoint of p.rootSet_L via R equals the adjoint of p.rootSet_K via R only if range of f equals top in the lattice.
Русский
Для многочлена p ∈ R[X], распадающегося над K, для любого алгебра-гомоморфа f: K → L сумма (адьяйн) p.rootSet_L через R равна диапазону p.rootSet_K через R тогда и только тогда, когда диапазон f равен верху.
LaTeX
$$$\\forall p:\\ Polynomial R,\\; Splits (\\mathrm{algebraMap} R K) p \\Rightarrow \\forall f:\\ K \\to_{R} L,\\; \\mathrm{Algebra.adjoin} R (p.\\text{rootSet }L) = f.\\text{range} \\Leftrightarrow \\mathrm{Algebra.adjoin} R (p.\\text{rootSet }K) = \\top.$$$
Lean4
theorem adjoin_rootSet_eq_range [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) :
Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤ :=
by
rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]
exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff
