Extensions of perfect fields are formally smooth

Every field extension L / K of a perfect field K is formally smooth: an algebra map L →ₐ[K] B ⧸ I lifts to L →ₐ[K] B along every square-zero ideal I. Mathlib proves this for L / K essentially of finite type (Algebra.FormallySmooth.of_perfectField), through a separating transcendence basis. A general extension need not have one: 𝔽_p(t ^ (1 / p ^ ∞)) is not separably generated over 𝔽_p. This file removes the finiteness hypothesis.

In characteristic zero a transcendence basis is still separating, and Mathlib's Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable applies. In characteristic p the proof uses the Frobenius map instead. Since I ^ 2 = 0 and p = 0 in B, the p-th power of a lift of z ∈ B ⧸ I does not depend on the lift. This gives a ring homomorphism B ⧸ I → B, and composed with the given map, the only possible lift ψ on the subfield L ^ p. Zorn's lemma gives a maximal lift extending it. It is defined on all of L: if a ∉ M, then a ^ p ∈ M and X ^ p - a ^ p is the minimal polynomial of a over M. Any lift b of the image of a has b ^ p = ψ(a ^ p), so a ↦ b extends the lift to M(a).

This is the input of Cohen's structure theorem for complete local rings in equal characteristic, which constructs coefficient fields by lifting the identity of the residue field.

Main results

• TauCeti.formallySmooth_of_perfectField: every field extension of a perfect field is formally smooth.

References

• A. Grothendieck, Éléments de géométrie algébrique IV, Première partie, Publ. Math. IHÉS 20 (1964), Chapitre 0, Théorème 19.6.1.
• H. Matsumura, Commutative Ring Theory, Cambridge University Press, 1986, Theorem 26.9 and Section 28.

The chain argument for partial lifts follows Mathlib's IntermediateField.Lifts, whose target is a field, adapted here to a ring target.

@[instance 100]

instance TauCeti.formallySmooth_of_perfectField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [PerfectField K] : Algebra.FormallySmooth K L

Every field extension of a perfect field is formally smooth: a K-algebra map from L to B ⧸ I, for a square-zero ideal I, lifts to B. No finiteness hypothesis on L / K is needed, unlike for Mathlib's Algebra.FormallySmooth.of_perfectField.