Residue fields in a constant field extension

Let F' = F · k' be a separable algebraic constant field extension of an algebraic function field F / k with exact constant field k, finite or not (an algebraic closure of a perfect k, for instance), and let P' be a place of F' / k' lying over the place P of F / k. The residue field of P' is the compositum of the residue field of P and the new constants:

F'_{P'} = F_P · k'.

In fact more is true: F'_{P'} is spanned as an F_P-vector space by the image of k'. When k' / k is finite, every residue class at P' is represented by a function regular at all the places over P, hence integral over 𝒪_P, and such a function is an 𝒪_P-combination of a k-basis of k' (TauCeti.Place.isIntegralBasis_constantBasis). Reducing that combination at P' writes the residue class as an F_P-combination of residues of constants. In general, a function representing a residue class at P' already lies in F · L for a finite subextension L of k' / k (TauCeti.exists_finiteDimensional_constantSubfield_of_mem_constantCompositum). The finite case writes its residue at the place below P' in F · L over the constants of L, and the residue-field map into F'_{P'} carries that expression to one over k'.

Consequently a place becomes rational as soon as the constants are enlarged enough: if k' / k is normal and the residue field F_P admits a k-embedding into k', every place of F' over P has degree one. Each element of F_P is a root of its minimal polynomial over k, which splits in k', so its residue in F'_{P'} is already a constant. For k' a separable closure of k, this applies to every place whose residue field is separable over k, hence to every place when k is perfect.

Main results

• TauCeti.Place.span_range_algebraMap_residueField_eq_top_of_constantCompositum_eq_top: F'_{P'} is spanned over F_P by the image of k'.
• TauCeti.Place.adjoin_range_algebraMap_residueField_eq_top_of_constantCompositum_eq_top: F'_{P'} = F_P · k' (Stichtenoth, Theorem 3.6.3(g)).
• TauCeti.Place.degree_eq_one_of_constantCompositum_eq_top: a place over P is rational when k' / k is normal and F_P embeds into k' over k.
• TauCeti.Place.card_le_encard_setOf_degree_eq_one_of_constantCompositum_eq_top: F' / k' has at least as many rational places as there are places of F whose residue fields embed into k'.
• TauCeti.Place.map_map_algebraMap_integers_eq_minpoly_of_constantCompositum_eq_top: a polynomial over the valuation ring of the restriction that models the minimal polynomial of a primitive element of F / E still models it over E · k'.
• TauCeti.Place.exists_constantCompositum_eq_top_and_forall_degree_eq_one: a place with separable residue field becomes rational after a finite separable extension of constants.
• TauCeti.Place.exists_constantCompositum_eq_top_nonempty_algHom: finitely many residue fields separable over k embed into one finite Galois extension of constants.

Reference

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.6.3(g).

theorem TauCeti.Place.span_range_algebraMap_residueField_eq_top_of_constantCompositum_eq_top {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (P' : Place k' F') : Submodule.span (restrict k F P').ResidueField (Set.range ⇑(algebraMap k' P'.ResidueField)) = ⊤

The residue field of a constant field extension is spanned by the constants: for a separable algebraic constant field extension F' = F · k' of F / k with exact constant field k, finite or not, the residue field of a place P' of F' / k' is spanned over the residue field of the place below by the image of k'.

theorem TauCeti.Place.adjoin_range_algebraMap_residueField_eq_top_of_constantCompositum_eq_top {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (P' : Place k' F') : IntermediateField.adjoin (restrict k F P').ResidueField (Set.range ⇑(algebraMap k' P'.ResidueField)) = ⊤

The residue field of a constant field extension is a compositum (Stichtenoth, Theorem 3.6.3(g)): for a separable algebraic constant field extension F' = F · k' of F / k with exact constant field k, finite or not, the residue field of a place P' of F' / k' is generated over the residue field F_P of the place below by the constants: F'_{P'} = F_P · k'.

theorem TauCeti.Place.degree_eq_one_of_constantCompositum_eq_top {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] [Normal k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (P' : Place k' F') (φ : (restrict k F P').ResidueField →ₐ[k] k') : P'.degree = 1

A place becomes rational in a large enough normal constant field extension: for a separable normal algebraic constant field extension F' = F · k' of F / k with exact constant field k, finite or not, a place P' of F' / k' has degree one as soon as the residue field of the place below admits a k-embedding into k'.

theorem TauCeti.Place.card_le_encard_setOf_degree_eq_one_of_constantCompositum_eq_top {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] [Normal k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) {T : Finset (Place k F)} (hT : ∀ P ∈ T, Nonempty (P.ResidueField →ₐ[k] k')) : ↑T.card ≤ {P' : Place k' F' | P'.degree = 1}.encard

Counting rational places in a large enough normal constant field extension: for a separable normal algebraic constant field extension F' = F · k' of F / k with exact constant field k, finite or not, if the residue fields of the places in a finite set T of places of F / k admit k-embeddings into k', then F' / k' has at least |T| rational places.

theorem TauCeti.Place.map_map_algebraMap_integers_eq_minpoly_of_constantCompositum_eq_top {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] {E : Type u_1} [Field E] [Algebra k E] [Algebra E F] [IsScalarTower k E F] [FiniteDimensional E F] [Algebra E F'] [IsScalarTower E F F'] [IsScalarTower k E F'] [Algebra k' ↥(constantCompositum E k' F')] [IsScalarTower k k' ↥(constantCompositum E k' F')] [FiniteDimensional E ↥(constantCompositum E k' F')] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) {y : F} (hy : E⟮y⟯ = ⊤) {P' : Place k' ↥(constantCompositum E k' F')} {φ : Polynomial ↥(restrict k E P').integers} (hφ : Polynomial.map (algebraMap (↥(restrict k E P').integers) E) φ = minpoly E y) : Polynomial.map (algebraMap ↥P'.integers ↥(constantCompositum E k' F')) (Polynomial.map (algebraMap ↥(restrict k E P').integers ↥P'.integers) φ) = minpoly (↥(constantCompositum E k' F')) ((algebraMap F F') y)

An integral model of a minimal polynomial survives a constant field extension: let y generate F over a subfield E containing k, over which F is finite, and let φ be a polynomial over 𝒪_P whose image over E is the minimal polynomial of y, where P is the restriction to E of a place P' of E · k'. Carried to 𝒪_{P'}, φ maps to the minimal polynomial of y over E · k'.

theorem TauCeti.Place.exists_constantCompositum_eq_top_and_forall_degree_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) [Algebra.IsSeparable k P.ResidueField] : ∃ (F' : IntermediateField F (AlgebraicClosure F)) (k' : IntermediateField k ↥F'), FiniteDimensional k ↥k' ∧ Algebra.IsSeparable k ↥k' ∧ constantCompositum F ↥k' ↥F' = ⊤ ∧ ∀ (P' : Place ↥k' ↥F'), restrict k F P' = P → P'.degree = 1

A place becomes rational after a finite separable extension of constants: if the residue field of a place P of F / k, with k exact, is separable over k, then some finite separable constant field extension F' = F · k', formed inside an algebraic closure of F, has only places of degree one over P.

theorem TauCeti.Place.exists_constantCompositum_eq_top_nonempty_algHom {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {E : Type u_1} [Field E] [Algebra k E] (hF : IsFunctionField k F) (hE : IsFunctionField k E) (s : Finset (Place k F)) (t : Finset (Place k E)) (hs : ∀ R ∈ s, Algebra.IsSeparable k R.ResidueField) (ht : ∀ Q ∈ t, Algebra.IsSeparable k Q.ResidueField) : ∃ (F' : IntermediateField F (AlgebraicClosure F)) (k' : IntermediateField k ↥F'), FiniteDimensional k ↥k' ∧ Normal k ↥k' ∧ Algebra.IsSeparable k ↥k' ∧ constantCompositum F ↥k' ↥F' = ⊤ ∧ (∀ R ∈ s, Nonempty (R.ResidueField →ₐ[k] ↥k')) ∧ ∀ Q ∈ t, Nonempty (Q.ResidueField →ₐ[k] ↥k')

Separable residue fields embed into one finite Galois extension of constants: the residue fields of finitely many places of function fields F / k and E / k, all separable over k, embed over k into one finite Galois extension k' of k, realised as a constant field extension F · k' inside an algebraic closure of F.