English
For a polynomial p over K and a field extension L, p is a splitting field over L if and only if p splits over L and the field generated by the roots of p in L is all of L.
Русский
Для полинома p над K и расширения L, p является полем развилки над L тогда и только тогда, когда p распадается над L и поле, порождаемое корнями p в L, равно всему L.
LaTeX
$$$\\text{Polynomial.IsSplittingField } K L\ \ \Longleftrightarrow\ \\bigl(\\text{Polynomial.Splits}(\\text{algebraMap } K L)\\ p\\bigr) \\land \\bigl(\\operatorname{adjoin}_K(p.rootSet L) = \\top\\bigr)$$$
Lean4
/-- Characterize `IsSplittingField` with `IntermediateField.adjoin` instead of `Algebra.adjoin`. -/
theorem isSplittingField_iff_intermediateField :
p.IsSplittingField K L ↔ p.Splits (algebraMap K L) ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤ :=
by
rw [← IntermediateField.toSubalgebra_injective.eq_iff,
IntermediateField.adjoin_algebraic_toSubalgebra fun _ ↦ isAlgebraic_of_mem_rootSet]
exact
⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩
-- Note: p.Splits (algebraMap F E) also works
