separableClosure_inf_perfectClosure

English

Let F ⊆ E be a field extension. Then the intersection of the separable closure of F in E with the perfect closure of F in E is as small as possible (the base field).

Русский

Пусть F ⊆ E — растяжение полей. Тогда пересечение разделимого замыкания F в E и идеального замыкания F в E равно нижнему элементу (базовому полю).

LaTeX

$$$\mathrm{separableClosure}(F,E) \cap \mathrm{perfectClosure}(F,E) = \bot$$$

Lean4

theorem separableClosure_inf_perfectClosure : separableClosure F E ⊓ perfectClosure F E = ⊥ :=
  haveI := (le_separableClosure_iff F E _).mp (inf_le_left (b := perfectClosure F E))
  haveI := (le_perfectClosure_iff F E _).mp (inf_le_right (a := separableClosure F E))
  eq_bot_of_isPurelyInseparable_of_isSeparable _

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