English
Let k be a field, K a field, and L an algebraic intermediate field of K over k. If k is algebraically closed, then L = ⊥.
Русский
Пусть k — поле, K — поле, и L — алгебраически замкнутое подполе K над k. Тогда L = ⊥.
LaTeX
$$$\forall {k K} [\mathrm{Field\;k}] [\mathrm{Field\;K}] [IsAlgClosed k] (L : \text{IntermediateField } k K) [Algebra.IsAlgebraic k L],\; L = \bot$$$
Lean4
/-- If `k` is algebraically closed, `K / k` is a field extension, `L / k` is an intermediate field
which is algebraic, then `L` is equal to `k`. A corollary of
`IsAlgClosed.algebraMap_surjective_of_isAlgebraic`. -/
@[stacks 09GQ "The result is the definition of algebraically closedness in Stacks Project. \
This statement is 09GR (4) ⟹ (1)."]
theorem eq_bot_of_isAlgClosed_of_isAlgebraic {k K : Type*} [Field k] [Field K] [IsAlgClosed k] [Algebra k K]
(L : IntermediateField k K) [Algebra.IsAlgebraic k L] : L = ⊥ :=
bot_unique fun x hx ↦
by
obtain ⟨y, hy⟩ := (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)).2 (⟨x, hx⟩ : L)
exact ⟨y, congr_arg (algebraMap L K) hy⟩
