Places with separable residue field

Let F / k be an algebraic function field, separable over a rational subfield k(x). Then F has a place P whose residue field is a separable extension of k of degree at most [F : k(x)]. Geometrically, a smooth proper curve has a closed point with separable residue field, of degree bounded by the degree of any separable map to the projective line.

Over a finite, hence perfect, field k any place over a rational place of k(x) will do. Over an infinite field the place is found over a rational place of k(x), of which there are infinitely many, at which the minimal polynomial of a primitive element of F / k(x) has separable reduction, which holds away from finitely many places. Kummer's theorem at such a place (TauCeti.Place.exists_restrict_eq_relativeDegree_eq_and_isSeparable) produces places of F above it whose residue fields are generated by a root of a separable irreducible factor of the reduction.

In genus zero the degree bound is two. If F / k has genus zero, exact constant field and a separating element, then F is separable over some k(x) of index at most two. Indeed, an anticanonical divisor B can be taken effective, of degree two, with ℓ(B) ≥ 3, and every nonconstant function in L(B) has index at most two. Away from characteristic two such an index is separable. In characteristic two, if two functions x, z ∈ L(B) with 1, x, z independent both had inseparable index two, then every square of F would lie in k(x) ∩ k(z), so the separating element would force k(x) = k(z). But a function of k(x) whose poles are bounded by (x)_∞ is a polynomial of degree at most one in x. So every genus-zero function field with exact constant field and a separating element has a place of degree at most two with separable residue field. Geometrically, a smooth proper curve of genus zero has a closed point whose residue field is separable of degree at most two over k. Over that residue field the curve has a rational point, and a curve of genus zero with a rational point is the projective line (TauCeti.nonempty_algEquiv_ratFunc_of_genus_eq_zero_of_divisor_degree_eq_one); this is the input for nodal reduction of curves of genus zero over a discrete valuation ring.

Main results

• TauCeti.exists_place_degree_le_finrank_and_isSeparable: a function field separable over k(x) has a place of degree at most [F : k(x)] with residue field separable over k.
• TauCeti.exists_finrank_adjoin_le_two_and_isSeparable_of_genus_eq_zero: a genus-zero function field with exact constant field and a separating element is separable over a rational subfield of index at most two.
• TauCeti.exists_place_degree_le_two_and_isSeparable_of_genus_eq_zero: a genus-zero function field with exact constant field and a separating element has a place of degree at most two whose residue field is separable over k.

References

• The Stacks Project, Chapter 55, Semistable Reduction, the case of genus zero.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.3.7 (Kummer's theorem).

Separable places over a separable rational subfield

theorem TauCeti.exists_place_degree_le_finrank_and_isSeparable {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : F) [Algebra.IsSeparable (↥k⟮x⟯) F] : ∃ (P : Place k F), P.degree ≤ Module.finrank (↥k⟮x⟯) F ∧ Algebra.IsSeparable k P.ResidueField

A function field separable over a rational subfield k(x) has a place of degree at most [F : k(x)] whose residue field is separable over k.

Genus zero

theorem TauCeti.exists_finrank_adjoin_le_two_and_isSeparable_of_genus_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : genus k F = 0) (t : F) [Algebra.IsSeparable (↥k⟮t⟯) F] : ∃ (x : F), Module.finrank (↥k⟮x⟯) F ≤ 2 ∧ Algebra.IsSeparable (↥k⟮x⟯) F

A genus-zero function field with exact constant field and a separating element is separable over a rational subfield of index at most two.

theorem TauCeti.exists_place_degree_le_two_and_isSeparable_of_genus_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : genus k F = 0) (t : F) [Algebra.IsSeparable (↥k⟮t⟯) F] : ∃ (P : Place k F), P.degree ≤ 2 ∧ Algebra.IsSeparable k P.ResidueField

A genus-zero function field with exact constant field and a separating element has a place of degree at most two whose residue field is separable over k. Geometrically, a smooth proper curve of genus zero has a closed point whose residue field is a separable extension of degree at most two.