isPurelyInseparable_adjoin_iff_pow_mem

English

If S ⊆ E and F ⟨S⟩/F is separable, then adjoin F S equals adjoin F S^{q^n} for any natural n, where q is the base field's exponential characteristic.

Русский

Если F⟨S⟩/F разделимо, то ADJOIN F S = ADJOIN F { x^{q^n} : x ∈ S } для любого n.

LaTeX

$$adjoin F S = adjoin F ((· ^ q ^ n) '' S)$$

Lean4

/-- If `F` is of exponential characteristic `q`, then `F(S) / F` is a purely inseparable extension
if and only if for any `x ∈ S`, `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`. -/
theorem isPurelyInseparable_adjoin_iff_pow_mem (q : ℕ) [hF : ExpChar F q] {S : Set E} :
    IsPurelyInseparable F (adjoin F S) ↔ ∀ x ∈ S, ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range := by
  simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q, Set.subset_def, SetLike.mem_coe]

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