isPurelyInseparable_adjoin_simple_iff_pow_mem

English

If F has characteristic q, then F⟮x⟯ is purely inseparable over F iff ∃ n with x^{q^n} in the base field image.

Русский

Если характеристика F равна q, то расширение F⟮x⟯ над F чисто бесразделимо тогда и только тогда, когда существует n такое, что x^{q^n} лежит в образе F в E.

LaTeX

$$IsPurelyInseparable F F⟮x⟯ ↔ ∃ n ∈ ℕ, x^{q^n} ∈ (algebraMap F E).range$$

Lean4

/-- If `F` is of exponential characteristic `q`, then `F⟮x⟯ / F` is a purely inseparable extension
if and only if `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`. -/
theorem isPurelyInseparable_adjoin_simple_iff_pow_mem (q : ℕ) [hF : ExpChar F q] {x : E} :
    IsPurelyInseparable F F⟮x⟯ ↔ ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range := by
  rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem q]

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