The places over a place in an algebraic constant field extension

Let F / k be an algebraic function field, let k' / k be an algebraic extension, finite or not, and let F' = F · k' be the compositum. This file proves that a place P of F / k has at most deg P places of F' / k' above it. In particular the fibre over P is finite even when F' / F is an infinite extension, and a rational place has exactly one place above it. Neither separability of k' / k nor exactness of k in F is assumed for these bounds.

For a finite extension k' / k this is a count in the fundamental inequality. A place P' over P has residue field containing both F_P and k', so the tower identity [k' : k] · deg P' = f(P' ∣ P) · deg P gives [k' : k] ≤ f(P' ∣ P) · deg P. Summing over the fibre and using ∑ e(P' ∣ P) f(P' ∣ P) ≤ [F' : F] ≤ [k' : k] bounds the number of places by deg P.

For an arbitrary algebraic k' / k, finitely many distinct places of F' are told apart by finitely many functions, one in the valuation ring of each place and outside that of another. These functions already lie in F · L for a finite subextension L / k (TauCeti.exists_finiteDimensional_constantSubfield_of_finset_subset_constantCompositum), so the places stay distinct after restriction to F · L, where the finite bound applies.

When k' / k is separable and k is the exact constant field of F, the degrees of the places over P add up to the degree of P:

∑_{P' ∣ P} deg P' = deg P.

This is Stichtenoth's Theorem 3.6.3(c), deg (Con A) = deg A, for the divisor A = P, and it holds for infinite k' / k as well. The place P is the only pole of some function z ∈ F. Every place over P has ramification index one, so the pole divisor of z in F' is m times the sum of the places over P, where m = -ord_P z, while in F it is m P. The degree of a pole divisor is the degree [F : k(z)], which does not change when the constants are extended. Equality #{P' ∣ P} = deg P holds when every place over P is rational. This is the case when k' / k is normal and the residue field of P embeds into k', for example when k' is a separable closure of k and the residue field of P is separable over k: then P splits into exactly deg P rational places.

The finiteness of the fibre is what the conorm of a divisor needs, so these statements are the first step in comparing the divisor theories of F / k and F · k' / k' for an infinite algebraic extension of constants, such as an algebraic closure of k.

Main results

• TauCeti.Place.card_le_degree_of_constantCompositum_eq_top: finitely many distinct places of F · k' over P number at most deg P.
• TauCeti.Place.finite_setOf_restrict_eq_of_constantCompositum_eq_top: the fibre over P is finite.
• TauCeti.Place.ncard_setOf_restrict_eq_le_degree_of_constantCompositum_eq_top: the fibre over P has at most deg P elements.
• TauCeti.Place.existsUnique_restrict_eq_of_degree_eq_one_of_constantCompositum_eq_top: exactly one place lies over a rational place.
• TauCeti.Place.finsum_degree_restrict_eq_degree_of_constantCompositum_eq_top: the degrees of the places over P add up to deg P in a separable algebraic constant field extension.
• TauCeti.Place.ncard_setOf_restrict_eq_eq_degree_of_constantCompositum_eq_top: there are exactly deg P places over P when k' / k is normal and the residue field of P embeds into k'.

References

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

theorem TauCeti.Place.card_le_degree_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.IsIntegral F F'] [Algebra.IsAlgebraic k k'] (hF : IsFunctionField k F) (h : constantCompositum F k' F' = ⊤) (P : Place k F) (t : Finset (Place k' F')) (ht : ∀ P' ∈ t, restrict k F P' = P) : t.card ≤ P.degree

A place has at most deg P places above it in a constant field extension: if F' = F · k' for an algebraic extension k' / k, finite or not, then finitely many distinct places of F' / k' lying over a place P of F / k number at most deg P. Neither separability of k' / k nor exactness of the constants is needed.

theorem TauCeti.Place.finite_setOf_restrict_eq_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.IsIntegral F F'] [Algebra.IsAlgebraic k k'] (hF : IsFunctionField k F) (h : constantCompositum F k' F' = ⊤) (P : Place k F) : {P' : Place k' F' | restrict k F P' = P}.Finite

A place has only finitely many places above it in a constant field extension: if F' = F · k' for an algebraic extension k' / k, finite or not, the places of F' / k' lying over a place of F / k form a finite set.

theorem TauCeti.Place.ncard_setOf_restrict_eq_le_degree_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.IsIntegral F F'] [Algebra.IsAlgebraic k k'] (hF : IsFunctionField k F) (h : constantCompositum F k' F' = ⊤) (P : Place k F) : {P' : Place k' F' | restrict k F P' = P}.ncard ≤ P.degree

A place has at most deg P places above it in a constant field extension: if F' = F · k' for an algebraic extension k' / k, finite or not, the set of places of F' / k' lying over a place P of F / k has at most deg P elements.

theorem TauCeti.Place.existsUnique_restrict_eq_of_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.IsIntegral F F'] [Algebra.IsAlgebraic k k'] (hF : IsFunctionField k F) (h : constantCompositum F k' F' = ⊤) {P : Place k F} (hP : P.degree = 1) : ∃! P' : Place k' F', restrict k F P' = P

A rational place has exactly one place above it in a constant field extension: if F' = F · k' for an algebraic extension k' / k, finite or not, and P is a place of F / k of degree one, then exactly one place of F' / k' lies over P.

theorem TauCeti.Place.finsum_degree_restrict_eq_degree_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) : ∑ᶠ (P' : Place k' F') (_ : P' ∈ {P' : Place k' F' | restrict k F P' = P}), P'.degree = P.degree

The degrees of the places over a place add up to its degree (Stichtenoth, Theorem 3.6.3(c), for a single place): if k is the exact constant field of F and F' = F · k' for a separable algebraic extension k' / k, finite or not, then for every place P of F / k,

∑_{P' ∣ P} deg P' = deg P,

where deg P' is the degree of P' over k'.

theorem TauCeti.Place.ncard_setOf_restrict_eq_eq_degree_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) (φ : P.ResidueField →ₐ[k] k') : {P' : Place k' F' | restrict k F P' = P}.ncard = P.degree

A place splits into deg P rational places once its residue field embeds into the constants: if k is the exact constant field of F, F' = F · k' for a separable normal algebraic extension k' / k, finite or not, and the residue field of a place P of F / k admits a k-embedding into k', then exactly deg P places of F' / k' lie over P. This applies to every place with residue field separable over k when k' is a separable closure of k.