English
Let F ⊆ K be a field extension and every element of K splits in L. Then for any x ∈ K, the set of values of x under all F-algebra embeddings K →_F L equals the root set of the minimal polynomial of x over F in L.
Русский
Пусть F ⊆ K и каждый элемент K распадается в L. Тогда образ x по всем F-гомоморфизмам K →_F L равен корневому множеству минимального полинома x над F в L.
LaTeX
$$$\{\psi(x) : \psi: K \to_F L\} = (minpoly_F(x)).rootSet L$$$
Lean4
/-- Let `K/F` be an algebraic extension of fields and `L` a field in which all the minimal
polynomial over `F` of elements of `K` splits. Then, for `x ∈ K`, the images of `x` by the
`F`-algebra morphisms from `K` to `L` are exactly the roots in `L` of the minimal polynomial
of `x` over `F`. -/
theorem range_eval_eq_rootSet_minpoly_of_splits {F K : Type*} (L : Type*) [Field F] [Field K] [Field L] [Algebra F L]
[Algebra F K] (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) [Algebra.IsAlgebraic F K] (x : K) :
(Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L :=
by
ext a
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))]
refine
⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦
IntermediateField.exists_algHom_of_splits_of_aeval (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, hA x⟩) ha⟩
rw [← hψ, Polynomial.aeval_algHom_apply ψ x, minpoly.aeval, map_zero]
