Finiteness of the absolute Frobenius

Let p be a prime and X a scheme locally of finite type over Spec R, where R is a perfect ring of characteristic p (for instance a perfect field). Then the absolute Frobenius F_X : X ⟶ X is a finite morphism (AlgebraicGeometry.Scheme.isFinite_frobenius). On an affine open U it is the p-th power map of Γ(X, U), which is finite because Γ(X, U) is of finite type over R and every element of R is a p-th power (TauCeti.powRingHom_finite).

The finite-type hypothesis cannot be dropped: the absolute Frobenius of the spectrum of the field of rational functions over 𝔽_p in infinitely many variables is not finite.

References

• The Stacks Project, Tag 0CC6, Frobenii.

theorem AlgebraicGeometry.Scheme.isFinite_frobenius {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] {R : Type u} [CommRing R] [ExpChar R p] [PerfectRing R p] (f : X ⟶ Spec ↧R) [LocallyOfFiniteType f] (hX : ↑p = 0) : IsFinite (X.frobenius p hX)

The absolute Frobenius of a scheme locally of finite type over a perfect ring is finite. For a scheme X locally of finite type over Spec R, with R a perfect ring of characteristic p, the absolute Frobenius F_X : X ⟶ X is a finite morphism.