Translates of a separating element are almost always prime elements

Let F / k be an algebraic function field and x a separating element, so that F / k(x) is a finite separable extension. Only finitely many places of F ramify over k(x) (TauCeti.Place.finite_setOf_differentExponent_ne_zero). A rational place P of F that is not a pole of x lies over a rational finite place of k(x), the zero of X - a for some a ∈ k; if P is unramified there, x - a is a prime element at P. A place of arbitrary degree that is not a pole of x lies over the zero of some irreducible q ∈ k[X], and if it is unramified there, q(x) is a prime element.

An unramified place has a separable residue extension over the place below it. Over an infinite field k there are infinitely many rational places X - a of k(x), and the places of F above all but finitely many of them are unramified, so their residue fields are separable over k. Over a finite field every residue field is separable. Either way a separably generated function field has infinitely many places with residue field separable over k, even when k is imperfect and F has only finitely many rational places.

Main results

• TauCeti.Place.differentExponent_ratFunc_eq_differentExponent_adjoin and TauCeti.Divisor.different_ratFunc_eq_different_adjoin: the different exponent and different divisor over RatFunc k induced by x agree with those over k⟮x⟯.
• TauCeti.Place.finite_setOf_forall_ord_sub_algebraMap_ne_one: at all but finitely many rational places that are not poles of a separating x, some x - a is a prime element.
• TauCeti.Place.finite_setOf_forall_irreducible_ord_aeval_ne_one: at all but finitely many places that are not poles of a separating x, some q(x) with q irreducible is a prime element.
• TauCeti.Place.infinite_setOf_isSeparable_residueField: if F / k has a separating element, infinitely many places of F have residue field separable over k.
• TauCeti.Place.infinite_setOf_isSeparable_residueField_of_finiteDimensional: the same holds for every subfield over which F is finite.

theorem TauCeti.Place.differentExponent_ratFunc_eq_differentExponent_adjoin {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (P : Place k F) : differentExponent k (RatFunc k) P = differentExponent k (↥k⟮x⟯) P

The different exponent over RatFunc k induced by x agrees with the different exponent over k⟮x⟯: for a separating element x and any place P of F, the different exponent of P is the same over RatFunc k through x and over k⟮x⟯.

theorem TauCeti.Place.finite_setOf_forall_ord_sub_algebraMap_ne_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : {P : Place k F | P.degree = 1 ∧ 0 ≤ P.ord x ∧ ∀ (a : k), P.ord (x - (algebraMap k F) a) ≠ 1}.Finite

Almost every rational place has a translate of x as a prime element: for a separating element x, only finitely many rational places P with ord_P x ≥ 0 admit no constant a with ord_P (x - a) = 1.

theorem TauCeti.Place.finite_setOf_forall_irreducible_ord_aeval_ne_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : {P : Place k F | 0 ≤ P.ord x ∧ ∀ (q : Polynomial k), Irreducible q → P.ord ((Polynomial.aeval x) q) ≠ 1}.Finite

Almost every place has a prime element q(x): for a separating element x, only finitely many places P with ord_P x ≥ 0 admit no irreducible q ∈ k[X] with ord_P q(x) = 1.

theorem TauCeti.Place.infinite_setOf_isSeparable_residueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : {P : Place k F | Algebra.IsSeparable k P.ResidueField}.Infinite

Infinitely many places have a separable residue field: if F / k has a separating element x, then infinitely many places of F have residue field separable over k. Over an infinite field these include the places above all but finitely many rational places X - a of k(x), where F / k(x) is unramified; over a finite field every place qualifies.

theorem TauCeti.Place.infinite_setOf_isSeparable_residueField_of_finiteDimensional {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {E : Type u_3} [Field E] [Algebra k E] [Algebra E F] [IsScalarTower k E F] [FiniteDimensional E F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : {Q : Place k E | Algebra.IsSeparable k Q.ResidueField}.Infinite

Infinitely many places of a subfield have a separable residue field: if F / k has a separating element and E ⊆ F is a subfield containing k over which F is finite, then infinitely many places of E have residue field separable over k. They include the restrictions of the places of F with separable residue field, and the restriction map has finite fibres.

theorem TauCeti.Divisor.different_ratFunc_eq_different_adjoin {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : different k F ⋯ = different k F ⋯

The different divisor over RatFunc k induced by x agrees with the different divisor over k⟮x⟯.