Kunz's theorem: regular rings have flat Frobenius

Let R be a regular ring of characteristic p. Then the absolute Frobenius R → R, a ↦ a ^ p, is flat (TauCeti.IsRegularRing.flat_frobenius). This is the implication from regularity to flatness in Kunz's characterization of regular rings in characteristic p.

For a regular local ring (R, 𝔪) of dimension d, Frobenius is a local homomorphism carrying a regular system of parameters x₁, …, x_d to x₁ ^ p, …, x_d ^ p. These generate an ideal with radical 𝔪, so they form a system of parameters, which is a regular sequence because R is Cohen–Macaulay. A local homomorphism of Noetherian local rings carrying generators of the maximal ideal of the source to a regular sequence is flat (RingHom.Flat.of_isWeaklyRegular_map), which gives the local case TauCeti.IsRegularLocalRing.flat_frobenius. This replaces the appeal to miracle flatness in the Stacks proof: the dimension count is only needed to see that the powers form a regular sequence. Flatness is local on the target, and Frobenius commutes with localization, so the local case gives the global one.

The theorems are stated for an exponential characteristic p, so that in characteristic zero, where p = 1 and Frobenius is the identity, they hold trivially.

Main results

• TauCeti.IsRegularLocalRing.flat_frobenius: Frobenius of a regular local ring is flat.
• TauCeti.IsRegularRing.flat_frobenius: Kunz's theorem, Frobenius of a regular ring is flat.

Frobenius is a local homomorphism by TauCeti.isLocalHom_frobenius, and regularity cannot be dropped: a ring of exponential characteristic p > 1 with flat Frobenius is reduced (TauCeti.isReduced_of_flat_frobenius).

References

• E. Kunz, Characterizations of regular local rings of characteristic p, Amer. J. Math. 91 (1969), 772–784.
• Stacks Project, Lemma 51.17.6, the implication from regularity to flatness.

theorem TauCeti.IsRegularLocalRing.flat_frobenius {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] [IsRegularLocalRing R] : (frobenius R p).Flat

Frobenius of a regular local ring is flat. In a regular local ring of exponential characteristic p, the p-th powers of a regular system of parameters form a regular sequence, so the Frobenius endomorphism is flat.

theorem TauCeti.IsRegularRing.flat_frobenius {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] [IsRegularRing R] : (frobenius R p).Flat

Kunz's theorem. The Frobenius endomorphism of a regular ring of exponential characteristic p is flat. Stacks, Lemma 51.17.6 (0EC0), the implication from regularity to flatness.