Flat Frobenius is injective and forces reducedness

Let R be a commutative ring of exponential characteristic p > 1. Frobenius induces the identity on the prime spectrum of R, so if it is flat it is faithfully flat, hence injective, and R is reduced. This is the obstruction to flatness of Frobenius on nonreduced rings, such as 𝔽_p[ε] ⧸ (ε²), where Frobenius kills ε. Kunz's theorem TauCeti.IsRegularRing.flat_frobenius gives flatness for regular rings.

Main results

• TauCeti.isReduced_of_flat_frobenius: a ring of exponential characteristic p > 1 with flat Frobenius is reduced.
• TauCeti.injective_frobenius_of_flat: flat Frobenius is injective.
• TauCeti.flat_iterateFrobenius: if Frobenius is flat, so is each of its iterates.

theorem TauCeti.isReduced_of_flat_frobenius {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (hp : 1 < p) (h : (frobenius R p).Flat) : IsReduced R

Flat Frobenius forces reducedness. If the Frobenius endomorphism of a ring of exponential characteristic p > 1 is flat, then the ring is reduced. Frobenius induces the identity on the prime spectrum, so flatness makes it faithfully flat, hence injective. In particular, regularity cannot be dropped from TauCeti.IsRegularRing.flat_frobenius: Frobenius of 𝔽_p[ε] ⧸ (ε²) kills ε and is not flat.

theorem TauCeti.injective_frobenius_of_flat {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (h : (frobenius R p).Flat) : Function.Injective ⇑(frobenius R p)

Flat Frobenius is injective.

theorem TauCeti.flat_iterateFrobenius {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (h : (frobenius R p).Flat) (n : ℕ) : (iterateFrobenius R p n).Flat

If the Frobenius endomorphism is flat, then so is each of its iterates.