English
If F is a field and E/F is separable with exponential characteristic q, then adjoining a set S to F is the same as adjoining all q^n-powers of elements of S.
Русский
Если F — поле, а E/F — separable с характеристикой q, то F(S) = F({x^{q^n} : x ∈ S}).
LaTeX
$$$\operatorname{adjoin} F S = \operatorname{adjoin} F \bigl((\cdot^{q^n})'' S\bigr)$$$
Lean4
/-- If `F` is a field of exponential characteristic `q`, `F(S) / F` is separable, then
`F(S) = F(S ^ (q ^ n))` for any natural number `n`. -/
theorem adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable (S : Set E) [Algebra.IsSeparable F (adjoin F S)] (q : ℕ)
[ExpChar F q] (n : ℕ) : adjoin F S = adjoin F ((· ^ q ^ n) '' S) :=
by
set L := adjoin F S
set M := adjoin F ((· ^ q ^ n) '' S)
have hi : M ≤ L := by
rw [adjoin_le_iff]
rintro _ ⟨y, hy, rfl⟩
exact pow_mem (subset_adjoin F S hy) _
letI := (inclusion hi).toAlgebra
haveI : Algebra.IsSeparable M (extendScalars hi) := Algebra.isSeparable_tower_top_of_isSeparable F M L
haveI : IsPurelyInseparable M (extendScalars hi) :=
by
haveI := expChar_of_injective_algebraMap (algebraMap F M).injective q
rw [extendScalars_adjoin hi, isPurelyInseparable_adjoin_iff_pow_mem M _ q]
exact fun x hx ↦ ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, rfl⟩
simpa only [extendScalars_restrictScalars, restrictScalars_bot_eq_self] using
congr_arg (restrictScalars F) (extendScalars hi).eq_bot_of_isPurelyInseparable_of_isSeparable
