The p-th power map of a ring in which a prime p vanishes

If p is a prime and p = 0 in a commutative semiring R, then x ↦ x ^ p is a ring endomorphism of R. Mathlib's frobenius R p packages this under the hypothesis ExpChar R p, which the zero ring does not satisfy for a prime p. The sections of the structure sheaf of a scheme over 𝔽_p include the zero ring (the sections over the empty open), so the absolute Frobenius of such a scheme is built from TauCeti.powRingHom, which only asks that p vanish in R.

Main definitions

• TauCeti.powRingHom R p h: the ring endomorphism x ↦ x ^ p of R, for h : (p : R) = 0.

Main results

• TauCeti.powRingHom_eq_frobenius: when R has exponential characteristic p, it is frobenius R p.

def TauCeti.powRingHom (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ↑p = 0) : R →+* R

The p-th power map x ↦ x ^ p on a commutative semiring in which the prime p vanishes, as a ring endomorphism. Unlike frobenius R p, it is defined for the zero ring.

@[simp]

theorem TauCeti.powRingHom_apply {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ↑p = 0) (x : R) : (powRingHom R p h) x = x ^ p

theorem TauCeti.powRingHom_eq_frobenius {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [ExpChar R p] (h : ↑p = 0) : powRingHom R p h = frobenius R p

When R has exponential characteristic p, the p-th power map is the Frobenius.