English
If every element of a set S has its minpoly splitting in L, then every element of the intermediate field adjoin F S also splits in L.
Русский
Если для каждого элемента из S минимальный полином распадается в L, то и любой элемент адьйона поля F S распадается в L.
LaTeX
$$theorem splits_of_mem_adjoin {L} [Field L] [Algebra F L] {S : Set K} (splits : ∀ x ∈ S, IsIntegral F x ∧ (minpoly F x).Splits (algebraMap F L)) {x : K} (hx : x ∈ adjoin F S) : (minpoly F x).Splits (algebraMap F L)$$
Lean4
/-- If a set of algebraic elements in a field extension `K/F` have minimal polynomials that
split in another extension `L/F`, then all minimal polynomials in the intermediate field
generated by the set also split in `L/F`. -/
@[stacks 0BR3 "first part"]
theorem splits_of_mem_adjoin {L} [Field L] [Algebra F L] {S : Set K}
(splits : ∀ x ∈ S, IsIntegral F x ∧ (minpoly F x).Splits (algebraMap F L)) {x : K} (hx : x ∈ adjoin F S) :
(minpoly F x).Splits (algebraMap F L) :=
by
let E : IntermediateField F L := ⨆ x : S, adjoin F ((minpoly F x.val).rootSet L)
have normal : Normal F E :=
normal_iSup (h := fun x ↦ Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField (splits x x.2).2))
have : ∀ x ∈ S, (minpoly F x).Splits (algebraMap F E) := fun x hx ↦
splits_of_splits (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩
convert splits_comp_of_splits _ E.val.toRingHom (normal.splits <| φ ⟨x, hx⟩)
rw [minpoly.algHom_eq _ φ.injective, ← minpoly.algHom_eq _ (adjoin F S).val.injective, val_mk]
