The places of the rational function field

The rational function field k(x) is the base case of the theory of algebraic function fields, and this file determines all of its places. Besides the finite places P_p coming from the height-one primes of k[X] — supplied in general by TauCeti.FieldTheory.FunctionField.Place.Adic — there is exactly one further place, the place at infinity P_∞, packaged here from Mathlib's RatFunc.inftyValuation. Its order function is ord_∞ f = -f.intDegree, its residue field is k, and the finite place of a height-one prime generated by a monic irreducible polynomial q has residue field k[X] / (q), hence degree q.natDegree.

That these are all the places is Mathlib's Ostrowski theorem for k(X), RatFunc.valuation_isEquiv_infty_or_adic, read in place vocabulary: because the valuation of a place is normalized, equivalence of valuations is equality of places, and the Xor of Ostrowski becomes the bijection TauCeti.Place.ratFuncEquiv.

Main definitions

• TauCeti.Place.infty: the place at infinity of k(x).
• TauCeti.Place.inftyResidueFieldEquiv: the identification of its residue field with k.
• TauCeti.Place.adicOfIrreducible: the finite place of an irreducible polynomial q, with TauCeti.Place.adicOfIrreducibleResidueFieldEquiv identifying its residue field with k[X]/(q).
• TauCeti.Place.ratFuncEquiv and TauCeti.Place.ratFuncEquivMonicIrreducible: the classification of the places of k(x), indexed by the height-one primes of k[X] and by the monic irreducible polynomials respectively.
• TauCeti.Place.ratFuncDegreeOneEquiv: the rational places of k(x) are ℙ¹(k) = k ∪ {∞}.

Main results

• TauCeti.Place.ord_infty: ord_∞ f = -f.intDegree, with TauCeti.Place.isUniformizer_infty exhibiting x⁻¹ as a prime element there.
• TauCeti.Place.degree_infty: the place at infinity is rational, deg P_∞ = 1 (Stichtenoth, Proposition 1.2.1(c)).
• TauCeti.Place.degree_ofPrime_eq_natDegree and TauCeti.Place.degree_adicOfIrreducible: a finite place whose prime is generated by q has degree q.natDegree, and each height-one prime of k[X] has such a generator, unique once it is required to be monic (Stichtenoth, Proposition 1.2.1(a)); TauCeti.Place.isUniformizer_adicOfIrreducible exhibits q as a prime element there.
• TauCeti.Place.eq_infty_or_exists_eq_ofPrime, TauCeti.Place.eq_infty_or_exists_eq_adicOfIrreducible and TauCeti.Place.ratFuncEquiv: these are all the places of k(x), and they are pairwise distinct (Stichtenoth, Theorem 1.2.2); TauCeti.Place.adicOfIrreducible_eq_adicOfIrreducible_iff says a finite place remembers exactly the associate class of its polynomial.
• TauCeti.Place.exists_algebraMap_notMem_integers_iff_eq_infty: the place at infinity is the only place of k(x) at which a polynomial has a pole.
• TauCeti.Place.eq_infty_or_exists_eq_adicOfIrreducible_X_sub_C and TauCeti.Place.ratFuncDegreeOneEquiv: the degree-one places are ℙ¹(k) = k ∪ {∞} (Stichtenoth, Corollary 1.2.3).

That k is the exact field of constants of k(x) — Proposition 1.2.1(d) — is TauCeti.algebraicClosure_ratFunc.

Implementation notes

RatFunc.inftyValuation is stated for a fixed DecidableEq (RatFunc k) instance. The place at infinity fixes that instance to Classical.decEq, and TauCeti.Place.valuation_infty transports the identification to any other instance, all such instances being equal.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.2.
• The valuation at infinity that this file packages as a place is Mathlib/FieldTheory/RatFunc/Valuation.lean (Anne Baanen, Ashvni Narayanan), and the Ostrowski theorem that the classification repackages is Mathlib/NumberTheory/RatFunc/Ostrowski.lean (María Inés de Frutos-Fernández, Xavier Généreux).

The place at infinity

noncomputable def TauCeti.Place.infty (k : Type u_1) [Field k] : Place k (RatFunc k)

The place at infinity of the rational function field: the normalized valuation with v_∞ f = exp (f.intDegree) for f ≠ 0, for which x⁻¹ is a prime element (Stichtenoth, Proposition 1.2.1(c)).

Equations

• TauCeti.Place.infty k = { valuation := RatFunc.inftyValuation k, valuation_surjective := ⋯, isTrivialOn := ⋯ }

theorem TauCeti.Place.valuation_infty (k : Type u_1) [Field k] [inst : DecidableEq (RatFunc k)] : (infty k).valuation = RatFunc.inftyValuation k

theorem TauCeti.Place.valuation_infty_apply {k : Type u_1} [Field k] {f : RatFunc k} (hf : f ≠ 0) : (infty k).valuation f = WithZero.exp f.intDegree

@[simp]

theorem TauCeti.Place.ord_infty {k : Type u_1} [Field k] (f : RatFunc k) : (infty k).ord f = -f.intDegree

The order function of the place at infinity is minus the degree. The junk values ord_∞ 0 = 0 and RatFunc.intDegree 0 = 0 match, so no nonvanishing hypothesis is needed.

theorem TauCeti.Place.isUniformizer_infty {k : Type u_1} [Field k] : (infty k).valuation.IsUniformizer RatFunc.X⁻¹

x⁻¹ is a prime element for the place at infinity (Stichtenoth, Proposition 1.2.1(c)).

theorem TauCeti.Place.valuation_infty_lt_one_iff {k : Type u_1} [Field k] {f : RatFunc k} (hf : f ≠ 0) : (infty k).valuation f < 1 ↔ f.intDegree < 0

The residue field at infinity

theorem TauCeti.Place.exists_valuation_infty_sub_lt_one {k : Type u_1} [Field k] {x : RatFunc k} (hx : (infty k).valuation x ≤ 1) : ∃ (c : k), (infty k).valuation (x - (algebraMap k (RatFunc k)) c) < 1

A rational function that is regular at infinity agrees there, to first order, with a constant: if deg f ≤ 0 then some c : k has deg (f - c) < 0. This is the surjectivity of the constants onto the residue field at infinity, in valuation form.

@[simp]

theorem TauCeti.Place.degree_infty (k : Type u_1) [Field k] : (infty k).degree = 1

The place at infinity is rational: every rational function regular at infinity agrees with a constant to first order, so deg P_∞ = 1 (Stichtenoth, Proposition 1.2.1(c)).

noncomputable def TauCeti.Place.inftyResidueFieldEquiv (k : Type u_1) [Field k] : k ≃ₐ[k] (infty k).ResidueField

The canonical k-algebra equivalence from k to the residue field at infinity.

Equations

• TauCeti.Place.inftyResidueFieldEquiv k = (TauCeti.Place.infty k).residueFieldEquivOfDegreeEqOne ⋯

@[simp]

theorem TauCeti.Place.inftyResidueFieldEquiv_apply (k : Type u_1) [Field k] (c : k) : (inftyResidueFieldEquiv k) c = (algebraMap k (infty k).ResidueField) c

instance TauCeti.Place.finiteDimensional_residueField_infty (k : Type u_1) [Field k] : Module.Finite k (infty k).ResidueField

The finite places

theorem TauCeti.Place.degree_ofPrime_eq_natDegree {k : Type u_1} [Field k] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial k)) {q : Polynomial k} (h : p.asIdeal = Ideal.span {q}) : (ofPrime k (RatFunc k) p).degree = q.natDegree

The residue field of a finite place of k(x) is k[X] / (q) for a generator q of its prime, so its degree is the degree of q (Stichtenoth, Proposition 1.2.1(a)).

The finite places, indexed by irreducible polynomials

noncomputable def TauCeti.Place.adicOfIrreducible {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : Place k (RatFunc k)

The finite place of k(x) attached to an irreducible polynomial q ∈ k[X]: the place of the height-one prime (q) (Stichtenoth, Proposition 1.2.1(a)). Every finite place is of this form, for a q that is unique once it is required to be monic.

Equations

• TauCeti.Place.adicOfIrreducible hq = TauCeti.Place.ofPrime k (RatFunc k) (IsDedekindDomain.HeightOneSpectrum.ofIrreducible hq)

theorem TauCeti.Place.adicOfIrreducible_def {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : adicOfIrreducible hq = ofPrime k (RatFunc k) (IsDedekindDomain.HeightOneSpectrum.ofIrreducible hq)

The defining equation of TauCeti.Place.adicOfIrreducible: it is the place of the height-one prime (q). This is deliberately not a simp lemma, since adicOfIrreducible is the simp normal form here: TauCeti.Place.valuation_adicOfIrreducible, TauCeti.Place.degree_adicOfIrreducible and the classification lemmas all rewrite it directly.

@[simp]

theorem TauCeti.Place.valuation_adicOfIrreducible {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : (adicOfIrreducible hq).valuation = IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc k) (IsDedekindDomain.HeightOneSpectrum.ofIrreducible hq)

theorem TauCeti.Place.isUniformizer_adicOfIrreducible {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : (adicOfIrreducible hq).valuation.IsUniformizer ((algebraMap (Polynomial k) (RatFunc k)) q)

An irreducible polynomial is a prime element for its own finite place.

@[simp]

theorem TauCeti.Place.degree_adicOfIrreducible {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : (adicOfIrreducible hq).degree = q.natDegree

The degree of the finite place of an irreducible polynomial is the degree of the polynomial (Stichtenoth, Proposition 1.2.1(a)).

@[simp]

theorem TauCeti.Place.adicOfIrreducible_eq_adicOfIrreducible_iff {k : Type u_1} [Field k] {q r : Polynomial k} (hq : Irreducible q) (hr : Irreducible r) : adicOfIrreducible hq = adicOfIrreducible hr ↔ Associated q r

Two irreducible polynomials define the same finite place exactly when they are associated (Stichtenoth, Proposition 1.2.1(a)): the place remembers the prime (q), and nothing more.

noncomputable def TauCeti.Place.adicOfIrreducibleResidueFieldEquiv {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : (Polynomial k ⧸ Ideal.span {q}) ≃ₐ[k] (adicOfIrreducible hq).ResidueField

The residue field of the finite place of an irreducible polynomial q is k[X] / (q) (Stichtenoth, Proposition 1.2.1(a)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Place.adicOfIrreducibleResidueFieldEquiv_mk {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) (r : Polynomial k) : (adicOfIrreducibleResidueFieldEquiv hq) ((Ideal.Quotient.mk (Ideal.span {q})) r) = (AlgEquiv.cast ⋯) ((algebraMap (Polynomial k) (ofPrime k (RatFunc k) (IsDedekindDomain.HeightOneSpectrum.ofIrreducible hq)).ResidueField) r)

The classification

theorem TauCeti.Place.ofPrime_ne_infty (k : Type u_1) [Field k] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial k)) : ofPrime k (RatFunc k) p ≠ infty k

No finite place of k(x) is the place at infinity.

@[simp]

theorem TauCeti.Place.adicOfIrreducible_ne_infty {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : adicOfIrreducible hq ≠ infty k

The finite place of an irreducible polynomial is not the place at infinity.

theorem TauCeti.Place.eq_infty_or_exists_eq_ofPrime {k : Type u_1} [Field k] (P : Place k (RatFunc k)) : P = infty k ∨ ∃ (p : IsDedekindDomain.HeightOneSpectrum (Polynomial k)), P = ofPrime k (RatFunc k) p

Every place of the rational function field is either the place at infinity or the place of a height-one prime of k[X] (Stichtenoth, Theorem 1.2.2). This repackages Mathlib's Ostrowski theorem RatFunc.valuation_isEquiv_infty_or_adic: normalization turns its equivalences of valuations into equalities of places.

theorem TauCeti.Place.eq_infty_or_exists_eq_adicOfIrreducible {k : Type u_1} [Field k] (P : Place k (RatFunc k)) : P = infty k ∨ ∃ (q : Polynomial k) (hq : Irreducible q), P = adicOfIrreducible hq

Stichtenoth, Theorem 1.2.2, in the vocabulary of TauCeti.Place.adicOfIrreducible: every place of k(x) is the place at infinity or the finite place of an irreducible polynomial.

theorem TauCeti.Place.exists_algebraMap_notMem_integers_iff_eq_infty {k : Type u_1} [Field k] {P : Place k (RatFunc k)} : (∃ (f : Polynomial k), (algebraMap (Polynomial k) (RatFunc k)) f ∉ P.integers) ↔ P = infty k

The place at infinity is the only place of k(x) infinite on the polynomial model: at every other place x is regular, hence so is every polynomial, while ord_∞ x = -1. This identifies the places at infinity of the affine model k[X] ⊆ k(x), in the form TauCeti.Place.compl_range_ofPrime takes.

@[simp]

theorem TauCeti.Place.exists_one_lt_valuation_algebraMap_iff_eq_infty {k : Type u_1} [Field k] {P : Place k (RatFunc k)} : (∃ (f : Polynomial k), 1 < P.valuation ((algebraMap (Polynomial k) (RatFunc k)) f)) ↔ P = infty k

A place of k(x) has valuation greater than one on a polynomial exactly when it is the place at infinity. This is the simp-normal form of exists_algebraMap_notMem_integers_iff_eq_infty.

noncomputable def TauCeti.Place.ratFuncEquiv (k : Type u_1) [Field k] : Option (IsDedekindDomain.HeightOneSpectrum (Polynomial k)) ≃ Place k (RatFunc k)

The places of the rational function field (Stichtenoth, Theorem 1.2.2): they are the height-one primes of k[X], each of which has a unique monic irreducible generator by IsDedekindDomain.HeightOneSpectrum.existsUnique_monic_irreducible_span, together with one further point, the place at infinity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Place.ratFuncEquiv_none (k : Type u_1) [Field k] : (ratFuncEquiv k) none = infty k

@[simp]

theorem TauCeti.Place.ratFuncEquiv_some (k : Type u_1) [Field k] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial k)) : (ratFuncEquiv k) (some p) = ofPrime k (RatFunc k) p

@[simp]

theorem TauCeti.Place.ratFuncEquiv_symm_infty (k : Type u_1) [Field k] : (ratFuncEquiv k).symm (infty k) = none

@[simp]

theorem TauCeti.Place.ratFuncEquiv_symm_ofPrime (k : Type u_1) [Field k] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial k)) : (ratFuncEquiv k).symm (ofPrime k (RatFunc k) p) = some p

noncomputable def TauCeti.Place.ratFuncEquivMonicIrreducible (k : Type u_1) [Field k] : Option { q : Polynomial k // q.Monic ∧ Irreducible q } ≃ Place k (RatFunc k)

The places of k(x), indexed by polynomials (Stichtenoth, Theorem 1.2.2): they are the monic irreducible polynomials of k[X] together with the place at infinity. This is TauCeti.Place.ratFuncEquiv composed with IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv.

Equations

• TauCeti.Place.ratFuncEquivMonicIrreducible k = IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv.optionCongr.trans (TauCeti.Place.ratFuncEquiv k)

@[simp]

theorem TauCeti.Place.ratFuncEquivMonicIrreducible_none (k : Type u_1) [Field k] : (ratFuncEquivMonicIrreducible k) none = infty k

@[simp]

theorem TauCeti.Place.ratFuncEquivMonicIrreducible_some (k : Type u_1) [Field k] (q : { q : Polynomial k // q.Monic ∧ Irreducible q }) : (ratFuncEquivMonicIrreducible k) (some q) = adicOfIrreducible ⋯

@[simp]

theorem TauCeti.Place.ratFuncEquivMonicIrreducible_symm_infty (k : Type u_1) [Field k] : (ratFuncEquivMonicIrreducible k).symm (infty k) = none

@[simp]

theorem TauCeti.Place.ratFuncEquivMonicIrreducible_symm_adicOfIrreducible (k : Type u_1) [Field k] (q : { q : Polynomial k // q.Monic ∧ Irreducible q }) : (ratFuncEquivMonicIrreducible k).symm (adicOfIrreducible ⋯) = some q

The rational places

theorem TauCeti.Place.adicOfIrreducible_X_sub_C_injective {k : Type u_1} [Field k] : Function.Injective fun (a : k) => adicOfIrreducible ⋯

Distinct constants give distinct places: X - a is recovered from the place it generates.

theorem TauCeti.Place.eq_infty_or_exists_eq_adicOfIrreducible_X_sub_C {k : Type u_1} [Field k] {P : Place k (RatFunc k)} (hP : P.degree = 1) : P = infty k ∨ ∃ (a : k), P = adicOfIrreducible ⋯

A rational place of k(x) is the place at infinity or the place of a linear polynomial (Stichtenoth, Corollary 1.2.3): a monic irreducible generator of degree one is an X - a.

noncomputable def TauCeti.Place.ratFuncDegreeOneEquiv (k : Type u_1) [Field k] : Option k ≃ { P : Place k (RatFunc k) // P.degree = 1 }

The rational places of k(x) are ℙ¹(k) = k ∪ {∞} (Stichtenoth, Corollary 1.2.3): a place of k(x) has degree one exactly when it is the place at infinity or the place of a linear polynomial X - a.

Equations

• TauCeti.Place.ratFuncDegreeOneEquiv k = Equiv.ofBijective (fun (a : Option k) => a.elim ⟨TauCeti.Place.infty k, ⋯⟩ fun (b : k) => ⟨TauCeti.Place.adicOfIrreducible ⋯, ⋯⟩) ⋯

@[simp]

theorem TauCeti.Place.ratFuncDegreeOneEquiv_none (k : Type u_1) [Field k] : ↑((ratFuncDegreeOneEquiv k) none) = infty k

@[simp]

theorem TauCeti.Place.ratFuncDegreeOneEquiv_some (k : Type u_1) [Field k] (a : k) : ↑((ratFuncDegreeOneEquiv k) (some a)) = adicOfIrreducible ⋯

@[simp]

theorem TauCeti.Place.ratFuncDegreeOneEquiv_symm_infty (k : Type u_1) [Field k] (h : (infty k).degree = 1) : (ratFuncDegreeOneEquiv k).symm ⟨infty k, h⟩ = none

@[simp]

theorem TauCeti.Place.ratFuncDegreeOneEquiv_symm_adicOfIrreducible (k : Type u_1) [Field k] (a : k) (h : (adicOfIrreducible ⋯).degree = 1) : (ratFuncDegreeOneEquiv k).symm ⟨adicOfIrreducible ⋯, h⟩ = some a