The rank of the Kähler differentials of a separably generated field extension

The proof of [TSPA, Tag 00TV] uses, as known, that dim_κ Ω[κ⁄k] = trdeg_k κ for a finitely generated separable extension κ/k; "separable" means separably generated [TSPA, Tags 030O, 030W]: there is a transcendence basis s with κ separable algebraic over k(s). The argument: k(s) is the fraction field of k[s] ≅ k[x_i]_{i ∈ s}, so Ω[k(s)⁄k] is free on the d x_i ([TSPA, Tags 00RX, 00RT], through Mathlib's mvPolynomialBasis, the formally étale base change along the isomorphism k[x] ≅ k[s], and Basis.ofIsLocalizedModule); κ/k(s) is separable algebraic, hence formally étale, so Ω[κ⁄k] ≅ κ ⊗_{k(s)} Ω[k(s)⁄k] (Mathlib's tensorKaehlerEquivOfFormallyEtale) is free of rank |s| = trdeg_k κ (Mathlib's cardinalMk_eq_trdeg). Over a perfect field every finitely generated extension has a separating transcendence basis (Mathlib's exists_isTranscendenceBasis_and_isSeparable_of_perfectField), and for a separable algebraic extension, such as the residue field of a closed point, Ω[κ⁄k] = 0, κ being formally unramified over k. These are the ingredients of the dimension formula dim S_𝔮 + trdeg_k κ(𝔮) = n for a smooth algebra in Hironaka/Algebra/RegularSmooth/Dimension.lean.

theorem Algebra.rank_kaehlerDifferential_eq_trdeg_of_isSeparable (k K : Type u) [Field k] [Field K] [Algebra k K] {s : Set K} (hs : IsTranscendenceBasis k Subtype.val) [Algebra.IsSeparable (↥(IntermediateField.adjoin k s)) K] : Module.rank K Ω[K⁄k] = trdeg k K

For a field extension K/k with a separating transcendence basis s (K separable over k(s)), the rank of Ω[K⁄k] is the transcendence degree of K/k (used in [TSPA, Tag 00TV]).

theorem Algebra.rank_kaehlerDifferential_eq_trdeg_of_perfectField (k K : Type u) [Field k] [Field K] [Algebra k K] [PerfectField k] [EssFiniteType k K] : Module.rank K Ω[K⁄k] = trdeg k K

For k perfect and K/k finitely generated (essentially of finite type), rank_K Ω[K⁄k] = trdeg_k K: every such extension has a separating transcendence basis.

theorem Algebra.subsingleton_kaehlerDifferential_of_isSeparable (k K : Type u) [Field k] [Field K] [Algebra k K] [Algebra.IsSeparable k K] : Subsingleton Ω[K⁄k]

For K/k separable algebraic, Ω[K⁄k] = 0: K is formally unramified over k.