The dimension of a smooth local ring

For S standard smooth of relative dimension n over a perfect field k and a prime 𝔮, with R = S_𝔮 and κ = κ(𝔮): R is regular (Hironaka/Algebra/RegularSmooth/SmoothImpliesRegular.lean), so dim R = dim_κ 𝔪/𝔪²; the conormal sequence is short exact (Cotangent.lean), so dim_κ 𝔪/𝔪² + dim_κ Ω[κ⁄k] = dim_κ κ ⊗[R] Ω[R⁄k]; and κ ⊗[R] Ω[R⁄k] = κ ⊗[S] Ω[S⁄k] has dimension n (Ω[S⁄k] is free of rank n; Ω[R⁄k] = R ⊗[S] Ω[S⁄k] because a localization is formally étale). Hence dim R + dim_κ Ω[κ⁄k] = n. With dim_κ Ω[κ⁄k] = trdeg_k κ (Trdeg.lean) this is the formula dim S_𝔮 + trdeg_k κ(𝔮) = n of Sta, Tag 0A21, (10); at a maximal ideal κ is finite over k (Zariski's lemma, Mathlib's finite_of_finite_type_of_isJacobsonRing), hence separable algebraic over the perfect field k, so Ω[κ⁄k] = 0 and dim S_𝔮 = n. The dimension arithmetic is additive in WithBot ℕ∞, the transcendence degree entering through Cardinal.toENat. The scheme forms are in Hironaka/Algebra/RegularSmooth/SchemeForms.lean.

theorem Algebra.IsStandardSmoothOfRelativeDimension.ringKrullDim_localization_add_finrank_kaehlerDifferential_residueField {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [PerfectField k] (n : ℕ) [IsStandardSmoothOfRelativeDimension n k S] (𝔮 : Ideal S) [𝔮.IsPrime] : ringKrullDim (Localization.AtPrime 𝔮) + ↑(Module.finrank 𝔮.ResidueField Ω[𝔮.ResidueField⁄k]) = ↑n

The core count: for S standard smooth of relative dimension n over a perfect field k and 𝔮 a prime, dim S_𝔮 + dim_κ Ω[κ(𝔮)⁄k] = n, with κ = κ(𝔮) the residue field.

theorem Algebra.IsStandardSmoothOfRelativeDimension.ringKrullDim_localization_add_trdeg_residueField {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [PerfectField k] (n : ℕ) [IsStandardSmoothOfRelativeDimension n k S] (𝔮 : Ideal S) [𝔮.IsPrime] : ringKrullDim (Localization.AtPrime 𝔮) + ↑(Cardinal.toENat (trdeg k 𝔮.ResidueField)) = ↑n

For k perfect and S standard smooth of relative dimension n over k, dim S_𝔮 + trdeg_k κ(𝔮) = n at every prime 𝔮 [TSPA, Tag 0A21, (10)].

theorem Algebra.IsStandardSmoothOfRelativeDimension.ringKrullDim_localization_of_isMaximal {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [PerfectField k] (n : ℕ) [IsStandardSmoothOfRelativeDimension n k S] (𝔮 : Ideal S) [𝔮.IsMaximal] : ringKrullDim (Localization.AtPrime 𝔮) = ↑n

For k perfect, S standard smooth of relative dimension n over k and 𝔮 a maximal ideal, dim S_𝔮 = n: the residue field is finite over k by Zariski's lemma.