English
If K/E/F is a field extension tower and K over E has no nontrivial algebraic subextensions (i.e., is purely transcendental), then the image of algebraicClosure F E in K equals algebraicClosure F K.
Русский
Пусть K над E над F образует табличку косвенных расширений; если K над E является чисто трансцендентным, то образ алгебраического замыкания F над E в K равен алгебраическому замыканию F над K.
LaTeX
$$$ (\\operatorname{algebraicClosure}_F(E)).map(\\operatorname{IsScalarTower.toAlgHom} F E K) = \\operatorname{algebraicClosure}_F(K) \\quad\\text{(under } \\text{algebraicClosure } E K = \\perp\\text{)} $$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `K / E` has no non-trivial algebraic
subextensions (this means that it is purely transcendental),
then the image of `algebraicClosure F E` in `K` is equal to `algebraicClosure F K`. -/
theorem map_eq_of_algebraicClosure_eq_bot [Algebra E K] [IsScalarTower F E K] (h : algebraicClosure E K = ⊥) :
(algebraicClosure F E).map (IsScalarTower.toAlgHom F E K) = algebraicClosure F K :=
by
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
obtain ⟨y, rfl⟩ :=
mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2 (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)
exact ⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩
