le_perfectClosure_iff — Mathlib

English

For an intermediate field L, L ≤ perfectClosure F E iff L is purely inseparable over F.

Русский

Для промежуточного поля L выполняется L ≤ perfectClosure F E тогда и только тогда, когда L чисто бесразделимо над F.

LaTeX

$$L ≤ perfectClosure F E ↔ IsPurelyInseparable F L$$

Lean4

/-- An intermediate field of `E / F` is contained in the relative perfect closure of `F` in `E`
if and only if it is purely inseparable over `F`. -/
theorem le_perfectClosure_iff (L : IntermediateField F E) : L ≤ perfectClosure F E ↔ IsPurelyInseparable F L :=
  by
  refine ⟨fun h ↦ (isPurelyInseparable_iff_pow_mem F (ringExpChar F)).2 fun x ↦ ?_, fun _ ↦ le_perfectClosure F E L⟩
  obtain ⟨n, y, hy⟩ := h x.2
  exact ⟨n, y, (algebraMap L E).injective hy⟩

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