English
If the separable closure over E to K collapses to ⊥, then the image equals the closure over F.
Русский
Если разделимое замыкание над E в K равно ⊥, то образ равен разделимому замыканию над F.
LaTeX
$$If separableClosure E K = ⊥ then (separableClosure F E).map (IsScalarTower.toAlgHom F E K) = separableClosure F K$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `K / E` has no non-trivial separable
subextensions (when `K / E` is algebraic, this means that it is purely inseparable),
then the image of `separableClosure F E` in `K` is equal to `separableClosure F K`. -/
theorem map_eq_of_separableClosure_eq_bot [Algebra E K] [IsScalarTower F E K] (h : separableClosure E K = ⊥) :
(separableClosure F E).map (IsScalarTower.toAlgHom F E K) = separableClosure F K :=
by
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
obtain ⟨y, rfl⟩ :=
mem_bot.1 <| h ▸ mem_separableClosure_iff.2 (IsSeparable.tower_top E <| mem_separableClosure_iff.1 hx)
exact ⟨y, (map_mem_separableClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩
