The degree of a place of an algebraic function field is finite

The residue field F_P of a place P of F / k is an extension of the constants k, and its degree deg P = [F_P : k] is the weight a place carries in a divisor. This file proves that the degree is finite and bounded, which is Stichtenoth, Algebraic Function Fields and Codes, Proposition 1.1.15: for every x : F whose order at P is nonzero,

1 ≤ deg P ≤ [F : k(x)].

The bound is what guards the junk value of Module.finrank in the definition TauCeti.Place.degree, so from here on the degree of a place of an algebraic function field is a genuine positive natural number.

Main results

• TauCeti.Place.linearIndependent_over_adjoin_of_linearIndependent_residue: the heart of the matter. If x has nonzero order at P, then elements of 𝒪_P whose residues are linearly independent over k are themselves linearly independent over k(x).
• TauCeti.Place.finiteDimensional_residueField_of_ord_ne_zero and TauCeti.Place.finiteDimensional_residueField: the residue field of a place of an algebraic function field is a finite extension of the constants.
• TauCeti.Place.degree_le_finrank_over_adjoin: deg P ≤ [F : k(x)] for every x with ord_P x ≠ 0. The lower bound 1 ≤ deg P is TauCeti.Place.one_le_degree_of_isFunctionField.
• TauCeti.Place.degree_eq_one_of_isAlgClosed_of_isFunctionField: over an algebraically closed field of constants every place of an algebraic function field is rational (Stichtenoth, Remark 1.1.17).

The auxiliary TauCeti.Place.residue_aeval_of_residue_eq_zero, that a polynomial expression in an element of the maximal ideal reduces to the constant term of the polynomial, is the residue computation Stichtenoth's argument turns on; it is reused by the bound on the zeros of a function in TauCeti.FieldTheory.FunctionField.Place.Zeros.

The rational places themselves are characterised in TauCeti.FieldTheory.FunctionField.Place.Basic, where no function-field hypothesis is needed.

Implementation notes

The linear-independence step is Stichtenoth's argument, run over the polynomial ring rather than over k(x): the family is shown to be linearly independent over the k-subalgebra k[x] = Algebra.adjoin k {x}, and LinearIndependent.iff_fractionRing then upgrades this to k(x) = k⟮x⟯, which is the fraction field of k[x] by Mathlib's IntermediateField.algebraAdjoinAdjoin instances. Clearing the common power of x from a relation is TauCeti.Polynomial.exists_common_X_pow_factor, which runs on the least exponent with a nonzero coefficient across the family, so no denominators ever appear.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 1.1.15 and Remark 1.1.17.

Residues of polynomial expressions in an element of the maximal ideal

@[simp]

theorem TauCeti.Place.residue_aeval_of_residue_eq_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {t : ↥P.integers} (ht : (IsLocalRing.residue ↥P.integers) t = 0) (p : Polynomial k) : (IsLocalRing.residue ↥P.integers) ((Polynomial.aeval t) p) = (algebraMap k P.ResidueField) (p.coeff 0)

If t lies in the maximal ideal of 𝒪_P, then the value of a polynomial p at t reduces to the constant term of p.

Linear independence over k(x) of a lift of a k-independent family of residues

theorem TauCeti.Place.linearIndependent_over_adjoin_of_linearIndependent_residue {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {x : F} (hx : P.ord x ≠ 0) {ι : Type u_1} {z : ι → ↥P.integers} (hz : LinearIndependent k fun (i : ι) => (IsLocalRing.residue ↥P.integers) (z i)) : LinearIndependent ↥k⟮x⟯ fun (i : ι) => ↑(z i)

The key step of Stichtenoth, Proposition 1.1.15. Let x be an element of nonzero order at a place P. If elements z i of the valuation ring 𝒪_P have residues that are linearly independent over the constants k, then the z i are themselves linearly independent over k(x).

Finiteness and the bound on the degree

theorem TauCeti.Place.rank_residueField_le_finrank_over_adjoin {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {x : F} (hx : P.ord x ≠ 0) [FiniteDimensional (↥k⟮x⟯) F] : Module.rank k P.ResidueField ≤ ↑(Module.finrank (↥k⟮x⟯) F)

The rank of the residue field over the constants is bounded by [F : k(x)] for every x whose order at P is nonzero, provided F is finite over k(x) (Stichtenoth, Proposition 1.1.15).

theorem TauCeti.Place.finiteDimensional_residueField_of_ord_ne_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {x : F} (hx : P.ord x ≠ 0) [FiniteDimensional (↥k⟮x⟯) F] : FiniteDimensional k P.ResidueField

The residue field of a place is a finite extension of the constants as soon as F is finite over k(x) for a single x of nonzero order at P (Stichtenoth, Proposition 1.1.15).

theorem TauCeti.Place.finiteDimensional_residueField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (hF : IsFunctionField k F) : FiniteDimensional k P.ResidueField

The residue field of a place of an algebraic function field is a finite extension of the constants (Stichtenoth, Proposition 1.1.15). This is what makes TauCeti.Place.degree a genuine invariant rather than a junk value.

theorem TauCeti.Place.degree_le_finrank_over_adjoin {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {x : F} (hx : P.ord x ≠ 0) [FiniteDimensional (↥k⟮x⟯) F] : P.degree ≤ Module.finrank (↥k⟮x⟯) F

Stichtenoth, Proposition 1.1.15: the degree of a place is bounded by [F : k(x)] for every x whose order at P is nonzero, provided F is finite over k(x).

theorem TauCeti.Place.one_le_degree_of_isFunctionField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (hF : IsFunctionField k F) : 1 ≤ P.degree

Stichtenoth, Proposition 1.1.15: the degree of a place of an algebraic function field is positive.

theorem TauCeti.Place.degree_eq_one_of_isAlgClosed_of_isFunctionField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) [IsAlgClosed k] (hF : IsFunctionField k F) : P.degree = 1

Stichtenoth, Remark 1.1.17: over an algebraically closed field of constants every place of an algebraic function field is rational.