Regular implies smooth

The implication (2) ⇒ (1) of [TSPA, Tag 00TV]: if S is a finite type algebra over the field k and 𝔮 ⊆ S a prime with S_𝔮 a regular local ring and residue field κ formally smooth over k, then S is smooth at 𝔮. The proof goes through Mathlib's Jacobian criterion as follows.

The presentation. Choose a surjection φ : k[x_1, …, x_N] → S, put Q = φ⁻¹(𝔮), P = k[x]_Q, R = S_𝔮; the localized map g : P → R is a local surjection with finitely generated kernel I, P is formally smooth over k with Ω[P⁄k] finite free (Presentation.lean), so Mathlib's Jacobian criterion (FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField) reduces smoothness of R over k to the injectivity of κ ⊗_P I → κ ⊗_P Ω[P⁄k], a ⊗ y ↦ a · (1 ⊗ d y), where κ = κ(R).

The kernel is generated by parameters. P is regular local (Polynomial.lean) and P/I ≅ R is regular local, so by [TSPA, Tag 00NR] (Hironaka/Algebra/Local/QuotientParameters.lean) I is generated by an initial segment x_1, …, x_c of a regular system of parameters of P. Hence κ ⊗_P I is spanned by the 1 ⊗ x_j, j ≤ c, whose images are the 1 ⊗ d x_j.

The images are independent. The classes of x_1, …, x_c are linearly independent in 𝔪_P/𝔪_P² (Hironaka/Algebra/Local/RegularSystem.lean), and the conormal map 𝔪_P/𝔪_P² → κ(P) ⊗_P Ω[P⁄k] is injective because κ(P) is formally smooth over k ([TSPA, Tag 00TU], Cotangent.lean): κ(P) ≅ κ(R) along g, and formal smoothness transports along this k-algebra isomorphism. So the 1 ⊗ d x_j are independent over κ(P) in κ(P) ⊗_P Ω[P⁄k], and then over κ(R) in κ(R) ⊗_P Ω[P⁄k], the two tensor products being identified semilinearly (linearIndependent_tmul_of_bijective_residueField_map).

Conclusion. A linear map that sends a spanning family to a linearly independent family is injective: writing an element of the kernel as ∑ a_j (1 ⊗ x_j), its image ∑ a_j (1 ⊗ d x_j) vanishes only if all a_j = 0. Over a perfect field every essentially finite type field extension is formally smooth (Mathlib's FormallySmooth.of_perfectField), which gives the form used for schemes in Hironaka/Algebra/RegularSmooth/RegularSmoothEquiv.lean.

noncomputable def Algebra.residueFieldAlgEquivOfBijective {k : Type u_1} [CommRing k] {P : Type u_2} {L : Type u_3} [CommRing P] [CommRing L] [IsLocalRing P] [IsLocalRing L] [Algebra k P] [Algebra k L] [Algebra P L] [IsScalarTower k P L] [IsLocalHom (algebraMap P L)] (hbij : Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap P L))) : IsLocalRing.ResidueField P ≃ₐ[k] IsLocalRing.ResidueField L

A local k-algebra map P → L inducing a bijection of residue fields gives a k-algebra isomorphism κ(P) ≃ κ(L).

Equations

• Algebra.residueFieldAlgEquivOfBijective hbij = AlgEquiv.ofRingEquiv ⋯

theorem Algebra.FormallySmooth.residueField_of_bijective {k : Type u_1} [CommRing k] {P : Type u_2} {L : Type u_3} [CommRing P] [CommRing L] [IsLocalRing P] [IsLocalRing L] [Algebra k P] [Algebra k L] [Algebra P L] [IsScalarTower k P L] [IsLocalHom (algebraMap P L)] (hbij : Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap P L))) [FormallySmooth k (IsLocalRing.ResidueField L)] : FormallySmooth k (IsLocalRing.ResidueField P)

Formal smoothness of κ(L) over k transports to κ(P) along the residue field bijection.

theorem Algebra.linearIndependent_tmul_of_bijective_residueField_map {k : Type u_1} [CommRing k] {P : Type u_2} {L : Type u_3} [CommRing P] [CommRing L] [IsLocalRing P] [IsLocalRing L] [Algebra k P] [Algebra P L] [IsLocalHom (algebraMap P L)] (hbij : Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap P L))) {ι : Type u_4} (v : ι → Ω[P⁄k]) (hv : LinearIndependent (IsLocalRing.ResidueField P) fun (i : ι) => 1 ⊗ₜ[P] v i) : LinearIndependent (IsLocalRing.ResidueField L) fun (i : ι) => 1 ⊗ₜ[P] v i

A family 1 ⊗ v_i linearly independent over κ(P) in κ(P) ⊗[P] Ω[P⁄k] is linearly independent over κ(L) in κ(L) ⊗[P] Ω[P⁄k] when P → L induces a bijection of residue fields: the two tensor products are identified along the residue field isomorphism, semilinearly.

theorem Algebra.IsSmoothAt.of_isRegularLocalRing {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [FiniteType k S] (𝔮 : Ideal S) [𝔮.IsPrime] [IsRegularLocalRing (Localization.AtPrime 𝔮)] [FormallySmooth k 𝔮.ResidueField] : IsSmoothAt k 𝔮

If S_𝔮 is a regular local ring and its residue field is formally smooth over k, then the finite type k-algebra S is smooth at 𝔮: the implication (2) ⇒ (1) of [TSPA, Tag 00TV], proved through Mathlib's Jacobian criterion, [TSPA, Tag 00NR] and [TSPA, Tag 00TU] as in the module docstring.

theorem Algebra.IsSmoothAt.of_isRegularLocalRing_of_perfectField {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [PerfectField k] [FiniteType k S] (𝔮 : Ideal S) [𝔮.IsPrime] [IsRegularLocalRing (Localization.AtPrime 𝔮)] : IsSmoothAt k 𝔮

For k perfect, S_𝔮 regular implies S smooth at 𝔮 over k ([TSPA, Tag 00TV], (2) ⇒ (1)): the residue field of S_𝔮 is essentially of finite type over k, hence formally smooth over the perfect field k.