English
For a reduced ring R of characteristic p with p-th Frobenius endomorphism, surjectivity of Frobenius implies that R is perfect (Frobenius is bijective).
Русский
Для редуцированного кольца R характеристики p сюръективность Фробениуса приводит к тому, что R совершенное (Фробениус биективен).
LaTeX
$$$\\operatorname{Surjective}(\\mathrm{frobenius}_{R,p}) \\Rightarrow \\mathrm{PerfectRing}_{p}(R)$$$
Lean4
/-- For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.
-/
theorem ofSurjective (R : Type*) (p : ℕ) [CommRing R] [ExpChar R p] [IsReduced R] (h : Surjective <| frobenius R p) :
PerfectRing R p :=
⟨frobenius_inj R p, h⟩
