English
If K/E/F is a field extension tower with E/F algebraic, then adjoin_E(separableClosure F K) = separableClosure E K.
Русский
Если K/ E/ F — цепь расширений полей, и E/F алгебраично, то adjoin_E(separableClosure F K) = separableClosure E K.
LaTeX
$$$\operatorname{adjoin}_E\bigl(\operatorname{separableClosure}_F K\bigr) = \operatorname{separableClosure}_E K$$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then
`E` adjoin `separableClosure F K` is equal to `separableClosure E K`. -/
theorem adjoin_eq_of_isAlgebraic [Algebra.IsAlgebraic F E] : adjoin E (separableClosure F K) = separableClosure E K :=
by
set S := separableClosure E K
have h := congr_arg lift (adjoin_eq_of_isAlgebraic_of_isSeparable (F := F) S)
rw [lift_top, lift_adjoin] at h
haveI : IsScalarTower F S K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
rw [← h, ← map_eq_of_separableClosure_eq_bot F (separableClosure_eq_bot E K)]
simp only [S, coe_map, IsScalarTower.coe_toAlgHom', IntermediateField.algebraMap_apply]
