Separably generated algebraic function fields

An algebraic function field over a perfect field admits a separating element: a transcendental element x over which the function field is finite and separable. This supplies the parameter needed for the differential calculus of an algebraic function field in arbitrary characteristic, while keeping the more general results over imperfect fields stated with an explicit separating element.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.10.2 and Section IV.1.

theorem TauCeti.IsFunctionField.exists_transcendental_and_isSeparable_adjoin_of_perfectField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) : ∃ (x : F), Transcendental k x ∧ Algebra.IsSeparable (↥k⟮x⟯) F

A function field over a perfect field is separably generated (Stichtenoth, Proposition 3.10.2): it has a transcendental element x such that F / k(x) is separable. Finiteness over k(x) follows separately from TauCeti.IsFunctionField.finiteDimensional_adjoin.