eq_bot_of_isSepClosed_of_isSeparable

English

If L is an intermediate field of K with L/k separable and k separably closed, then L = ⊥ (i.e., L = k).

Русский

Если L — промежуточное поле K над k, и L/k сепарабельно, и k сепарабельное замкнутое, то L = ⊥ (то есть L = k).

LaTeX

$$L = ⊥$$

Lean4

/-- If `k` is separably closed, `K / k` is a field extension, `L / k` is an intermediate field
which is separable, then `L` is equal to `k`. A corollary of `IsSepClosed.algebraMap_surjective`. -/
theorem eq_bot_of_isSepClosed_of_isSeparable [IsSepClosed k] [Algebra k K] (L : IntermediateField k K)
    [Algebra.IsSeparable k L] : L = ⊥ :=
  bot_unique fun x hx ↦ by
    obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩
    exact ⟨y, congr_arg (algebraMap L K) hy⟩

Похожие утверждения