English
If E is separably closed, then SeparableClosure F E = ⊥ iff F is separably closed.
Русский
Если E разделимо замкнуто, то SepClosure F E = ⊥ тогда и только тогда, когда F разделимо замкнуто.
LaTeX
$$separableClosure_eq_bot_iff (F:E) : SeparableClosure F E = ⊥ ↔ IsSepClosed F$$
Lean4
/-- If `E / F` is a field extension and `E` is separably closed, then the separable closure
of `F` in `E` is equal to `F` if and only if `F` is separably closed. -/
theorem separableClosure_eq_bot_iff [IsSepClosed E] : separableClosure F E = ⊥ ↔ IsSepClosed F :=
by
refine
⟨fun h ↦ IsSepClosed.of_exists_root _ fun p _ hirr hsep ↦ ?_, fun _ ↦
IntermediateField.eq_bot_of_isSepClosed_of_isSeparable _⟩
obtain ⟨x, hx⟩ := IsSepClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne' hsep
obtain ⟨x, rfl⟩ := h ▸ mem_separableClosure_iff.2 (hsep.of_dvd <| minpoly.dvd _ x hx)
exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩
