English
If E is a perfect field of characteristic p, then the relative perfect closure of E is again a perfect ring of characteristic p.
Русский
Если E — идеальное поле с степенью p, тогда относительное идеальное замыкание E также является идеальным кольцом с характеристикой p.
LaTeX
$$PerfectRing(F,E) :=> PerfectRing(⊤, p)$$
Lean4
/-- If `E` is a perfect field of exponential characteristic `p`, then the (relative) perfect closure
`perfectClosure F E` is perfect. -/
instance perfectRing (p : ℕ) [ExpChar E p] [PerfectRing E p] : PerfectRing (perfectClosure F E) p :=
.ofSurjective _ p fun x ↦ by
haveI := RingHom.expChar _ (algebraMap F E).injective p
obtain ⟨x', hx⟩ := surjective_frobenius E p x.1
obtain ⟨n, y, hy⟩ := (mem_perfectClosure_iff_pow_mem p).1 x.2
rw [frobenius_def] at hx
rw [← hx, ← pow_mul, ← pow_succ'] at hy
exact
⟨⟨x', (mem_perfectClosure_iff_pow_mem p).2 ⟨n + 1, y, hy⟩⟩, by simp_rw [frobenius_def, SubmonoidClass.mk_pow, hx]⟩
