English
If F ⊆ K is a normal extension and K/F is finite-dimensional, there exists a polynomial p in F[X] with K as its splitting field.
Русский
Если F ⊆ K образуют нормальное расширение и K конечномер над F, существует p ∈ F[X] такое, что K является его разложимым полем.
LaTeX
$$$\exists p \in F[X],\ IsSplittingField F K p$$$
Lean4
theorem exists_isSplittingField [h : Normal F K] [FiniteDimensional F K] : ∃ p : F[X], IsSplittingField F K p := by
classical
let s := Module.Basis.ofVectorSpace F K
refine ⟨∏ x, minpoly F (s x), splits_prod _ fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
refine fun x =>
Algebra.subset_adjoin
(Multiset.mem_toFinset.mpr <|
(mem_roots <| mt (Polynomial.map_eq_zero <| algebraMap F K).1 <| Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)
· exact minpoly.ne_zero (h.isIntegral (s x))
rw [IsRoot.def, eval_map, ← aeval_def, map_prod]
exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
