One-dimensionality of the Kähler differentials of a function field

Let k be a field and F a field extension of k containing an element x that is transcendental over k and separating, meaning that F is separable algebraic over the subfield k(x) it generates. This file proves that the module of Kähler differentials Ω[F⁄k] is then one-dimensional over F, with basis the differential d x; every differential is (dy/dx) · dx for a unique scalar.

An algebraic function field of one variable with a separating element is the motivating case: there F is moreover finite over k(x), which the basis construction does not need. Separability is not cosmetic — it is what the base-change argument runs on — so the general basis results carry it as a hypothesis. For a one-variable function field over a perfect field, the final theorem also proves the converse: x is separating exactly when d x is nonzero.

The proof is the base-change route: k(x)/k is a localization of the polynomial ring, whose differentials are free of rank one on d X, and F/k(x) is separable, hence formally étale (Algebra.FormallyEtale.of_isSeparable), so Ω[F⁄k] is the base change of Ω[k(x)⁄k] along k(x) → F by KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale.

Main results

• TauCeti.kaehlerBasisRatFunc: d X is a basis of Ω[k(X)⁄k].
• TauCeti.finrank_kaehlerDifferential_eq_one_of_separating: dim_F Ω[F⁄k] = 1.
• TauCeti.kaehlerBasisOfSeparating: d x is a basis of Ω[F⁄k].
• TauCeti.derivativeOfSeparating: differentiation y ↦ dy/dx with respect to x, as a k-derivation of F, with TauCeti.derivativeOfSeparating_smul_D the identity d y = (dy/dx) · dx and TauCeti.eq_derivativeOfSeparating its uniqueness.
• TauCeti.IsFunctionField.isSeparable_adjoin_iff_D_ne_zero: the differential criterion for a fixed parameter over a perfect field.

References

The result is Stichtenoth, Algebraic Function Fields and Codes, second edition, GTM 254, §IV.1: the differential module of a function field with a separating element x is one-dimensional with basis dx. The proof here is not his — he builds a differential module by hand from derivations, whereas this file reads the statement off Mathlib's base-change theory of Kähler differentials.

noncomputable def TauCeti.kaehlerBasisRatFunc (k : Type u_1) [Field k] : Module.Basis Unit (RatFunc k) Ω[RatFunc k⁄k]

d X is a basis of the module of Kähler differentials of the rational function field k(X) over k.

Equations

• TauCeti.kaehlerBasisRatFunc k = TauCeti.kaehlerBasisOfFormallyEtale k (Polynomial k) (RatFunc k) ((Module.Basis.singleton Unit (Polynomial k)).map (KaehlerDifferential.polynomialEquiv k).symm)

@[simp]

theorem TauCeti.kaehlerBasisRatFunc_apply (k : Type u_1) [Field k] (i : Unit) : (kaehlerBasisRatFunc k) i = (KaehlerDifferential.D k (RatFunc k)) RatFunc.X

theorem TauCeti.D_ne_zero_of_separating {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) : (KaehlerDifferential.D k F) x ≠ 0

The differential of a separating element is nonzero.

theorem TauCeti.finrank_kaehlerDifferential_eq_one_of_separating {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) : Module.finrank F Ω[F⁄k] = 1

The Kähler differentials of a separably generated extension of transcendence degree one are one-dimensional: if x is transcendental over k and F is separable over k(x), then Ω[F⁄k] is a one-dimensional F-vector space.

noncomputable def TauCeti.kaehlerBasisOfSeparating {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) : Module.Basis Unit F Ω[F⁄k]

The differential d x of a separating element x is a basis of Ω[F⁄k]; its coordinate function sends d y to the derivative dy/dx.

Equations

• TauCeti.kaehlerBasisOfSeparating hx = FiniteDimensional.basisSingleton Unit ⋯ ((KaehlerDifferential.D k F) x) ⋯

@[simp]

theorem TauCeti.kaehlerBasisOfSeparating_apply {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) (i : Unit) : (kaehlerBasisOfSeparating hx) i = (KaehlerDifferential.D k F) x

theorem TauCeti.span_D_eq_top_of_separating {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) : F ∙ (KaehlerDifferential.D k F) x = ⊤

The differential of a separating element spans all of Ω[F⁄k].

noncomputable def TauCeti.derivativeOfSeparating {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) : Derivation k F F

Differentiation with respect to a separating element x: the k-derivation of F sending y to the coordinate dy/dx of d y in the basis d x. Its derivation structure supplies the sum and product rules and the vanishing on k.

Equations

• TauCeti.derivativeOfSeparating hx = ((TauCeti.kaehlerBasisOfSeparating hx).coord ()).compDer (KaehlerDifferential.D k F)

@[simp]

theorem TauCeti.derivativeOfSeparating_smul_D {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) (y : F) : (derivativeOfSeparating hx) y • (KaehlerDifferential.D k F) x = (KaehlerDifferential.D k F) y

The defining property of dy/dx: it is the coordinate of d y in the basis d x.

theorem TauCeti.eq_derivativeOfSeparating {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) (y c : F) (hc : c • (KaehlerDifferential.D k F) x = (KaehlerDifferential.D k F) y) : c = (derivativeOfSeparating hx) y

dy/dx is the only scalar taking d x to d y.

@[simp]

theorem TauCeti.derivativeOfSeparating_self {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [Algebra.IsSeparable (↥k⟮x⟯) F] (hx : Transcendental k x) : (derivativeOfSeparating hx) x = 1

@[simp]

theorem TauCeti.IsFunctionField.isSeparable_adjoin_iff_D_ne_zero {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} [PerfectField k] (hF : IsFunctionField k F) : Algebra.IsSeparable (↥k⟮x⟯) F ↔ (KaehlerDifferential.D k F) x ≠ 0

An element of a one-variable function field over a perfect field is separating exactly when its universal differential is nonzero. Both sides fail for an algebraic x: its differential vanishes, while separability of F / k⟮x⟯ would make the function field algebraic over k.