Finiteness of the p-th power map

Let p be a prime and A a commutative ring in which p vanishes. The p-th power map TauCeti.powRingHom A p h : A →+* A is always integral: the power map sends the monic polynomial X ^ p - C a of the source to X ^ p - C (a ^ p), which vanishes at a. If moreover A is of finite type over a perfect ring R, then A is of finite type over its subring of p-th powers, because that subring contains the image of R; so the p-th power map is finite. This is the algebraic input to the finiteness of the absolute Frobenius of a scheme locally of finite type over a perfect field.

Without the finite-type hypothesis the p-th power map need not be finite: for instance it is not finite on the field of rational functions over 𝔽_p in infinitely many variables.

Main results

• TauCeti.powRingHom_isIntegral: the p-th power map is integral.
• TauCeti.powRingHom_finiteType: it is of finite type when A is of finite type over a perfect ring.
• TauCeti.powRingHom_finite: it is finite when A is of finite type over a perfect ring.

References

• The Stacks Project, Tag 0CC6, Frobenii.

theorem TauCeti.powRingHom_isIntegral {A : Type u_1} [CommRing A] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ↑p = 0) : (powRingHom A p h).IsIntegral

The p-th power map is integral: its image of X ^ p - C a is X ^ p - C (a ^ p), which vanishes at a.

theorem TauCeti.powRingHom_finiteType {A : Type u_1} [CommRing A] {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_2} [CommRing R] [ExpChar R p] [PerfectRing R p] (h : ↑p = 0) (f : R →+* A) (hf : f.FiniteType) : (powRingHom A p h).FiniteType

If A is of finite type over a perfect ring R, then the p-th power map of A is of finite type: the image of R consists of p-th powers.

theorem TauCeti.powRingHom_finite {A : Type u_1} [CommRing A] {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_2} [CommRing R] [ExpChar R p] [PerfectRing R p] (h : ↑p = 0) (f : R →+* A) (hf : f.FiniteType) : (powRingHom A p h).Finite

If A is of finite type over a perfect ring R, then the p-th power map of A is finite.