Frobenius and separating elements of a function field

This file proves the fixed-parameter part of Stichtenoth's separable-generation criterion. For a one-variable function field F / k over a perfect field of exponential characteristic p, an element outside the subfield F^p of Frobenius powers is separating. Consequently, a place at which the order of x is not divisible by p certifies that x is separating.

The proof combines three ingredients. A separating parameter exists over a perfect field; the rational function field has degree p over its p-th-power subfield; and the kernel of a nonzero derivation is an intermediate field. The first two facts give [F : F^p] = p. Since this degree is prime in positive characteristic, the kernel of a nonzero derivation that contains F^p must equal F^p.

Main results

• TauCeti.IsFunctionField.finrank_fieldRange_frobenius: [F : F^p] = p.
• TauCeti.IsFunctionField.D_eq_zero_iff_mem_fieldRange_frobenius: the kernel of the universal derivation is exactly F^p.
• TauCeti.IsFunctionField.transcendental_and_isSeparable_adjoin_of_not_dvd_ord: the valuation-order criterion.

Reference

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

theorem TauCeti.IsFunctionField.finrank_fieldRange_frobenius {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (p : ℕ) [ExpChar F p] : Module.finrank (↥(frobenius F p).fieldRange) F = p

The degree of a one-variable function field over its subfield of p-th powers is p. This is the degree computation underlying the fixed-parameter separability criterion.

theorem TauCeti.IsFunctionField.D_eq_zero_iff_mem_fieldRange_frobenius {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (p : ℕ) [ExpChar F p] [Fact (Nat.Prime p)] (x : F) : (KaehlerDifferential.D k F) x = 0 ↔ x ∈ (frobenius F p).fieldRange

The kernel of the universal derivation is the Frobenius subfield: in a one-variable function field over a perfect field, d x = 0 exactly when x is a p-th power. This identifies differential nonvanishing with the Frobenius-subfield obstruction used by separating criteria.

theorem TauCeti.IsFunctionField.transcendental_and_isSeparable_adjoin_of_not_dvd_ord {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (v : Valuation F (WithZero (Multiplicative ℤ))) (p : ℕ) [ExpChar F p] {x : F} (hx : ¬↑p ∣ v.ord x) : Transcendental k x ∧ Algebra.IsSeparable (↥k⟮x⟯) F

The valuation-order criterion for a separating element (Stichtenoth, Proposition 3.10.2): if the order of x at a discrete valuation is not divisible by the exponential characteristic p, then x is transcendental and F / k(x) is separable.