English
Let F ⊆ E ⊆ K be a field extension tower with E/F algebraic and K/E separable. Then the subfield generated by E and the separable closure of F in K equals K; i.e., adjoin_E(separableClosure_F K) = K.
Русский
Пусть F ⊆ E ⊆ K — цепь расширений полей, такая что E/F алгебраично, а K/E разделимо. Тогда порождаемое E вместе с сепарабельным замыканием F в K совпадает с K; т.е. adjoin_E(separableClosure_F K) = K.
LaTeX
$$$\operatorname{adjoin}_E\bigl(\operatorname{separableClosure}_F K\bigr) = K$$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic and `K / E`
is separable, then `E` adjoin `separableClosure F K` is equal to `K`. It is a special case of
`separableClosure.adjoin_eq_of_isAlgebraic`, and is an intermediate result used to prove it. -/
theorem adjoin_eq_of_isAlgebraic_of_isSeparable [Algebra.IsAlgebraic F E] [Algebra.IsSeparable E K] :
adjoin E (separableClosure F K : Set K) = ⊤ :=
top_unique fun x _ ↦ by
set S := separableClosure F K
set L := adjoin E (S : Set K)
have := Algebra.isSeparable_tower_top_of_isSeparable E L K
let i : S →+* L := Subsemiring.inclusion fun x hx ↦ subset_adjoin E (S : Set K) hx
let _ : Algebra S L := i.toAlgebra
let _ : SMul S L := Algebra.toSMul
have : IsScalarTower S L K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
have := Algebra.IsAlgebraic.trans F E K
have : IsPurelyInseparable S K := separableClosure.isPurelyInseparable F K
have := IsPurelyInseparable.tower_top S L K
obtain ⟨y, rfl⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable L K x
exact y.2
