Existence of places of an algebraic function field

Stichtenoth's existence theorem (Theorem 1.1.19) produces a place out of nothing but a subring and a proper nonzero ideal: if k ⊆ R ⊆ F and I is a proper nonzero ideal of R, then some place P of F / k has R ⊆ 𝒪_P and I ⊆ 𝔪_P. Its consequence (Corollary 1.1.20) is the statement that gives the divisor theory its substance: every element of F transcendental over k has both a zero and a pole, so ℙ_F is nonempty and the constants algebraicClosure k F are exactly the functions regular at every place.

Combined with weak approximation, the existence of poles shows that there are infinitely many places (Stichtenoth, Corollary 1.3.2): at finitely many places a single function could be given a zero everywhere, and such a function would be transcendental yet have no pole.

The Zorn's lemma half of Theorem 1.1.19 is Mathlib's Ideal.image_subset_nonunits_valuationSubring, which dominates a proper ideal of a subring of a field by a valuation subring. What is specific to function fields is that the resulting valuation subring is discrete, and that is TauCeti.Place.ofValuationSubring.

Main results

• TauCeti.Place.exists_forall_mem_integers_and_valuation_lt_one: Stichtenoth, Theorem 1.1.19.
• TauCeti.Place.exists_ord_pos and TauCeti.Place.exists_ord_neg: an element transcendental over the constants has a zero and a pole (Stichtenoth, Corollary 1.1.20).
• TauCeti.Place.nonempty: an algebraic function field has at least one place.
• TauCeti.Place.infinite: an algebraic function field has infinitely many places.
• TauCeti.Place.mem_algebraicClosure_iff_forall_mem_integers and TauCeti.Place.coe_algebraicClosure_eq_iInter_integers: algebraicClosure k F = ⋂_P 𝒪_P, the constants are the everywhere-regular functions.
• TauCeti.Place.exists_algebraMap_notMem_integers: every subring with fraction field F has a place at infinity.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.1.19 and Corollaries 1.1.20 and 1.3.2.

The existence theorem

theorem TauCeti.Place.exists_forall_mem_integers_and_valuation_lt_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {R : Subring F} (hkR : ∀ (c : k), (algebraMap k F) c ∈ R) {I : Ideal ↥R} (hI : I ≠ ⊤) (hI0 : I ≠ ⊥) : ∃ (P : Place k F), (∀ (r : ↥R), ↑r ∈ P.integers) ∧ ∀ a ∈ I, P.valuation ↑a < 1

Stichtenoth, Theorem 1.1.19. Let R be a subring of F containing the constants and let I be a proper nonzero ideal of R. Then some place of F / k has R inside its valuation ring and I inside its maximal ideal.

Mathlib's Ideal.image_subset_nonunits_valuationSubring supplies a valuation subring B of F with R ≤ B and I inside the nonunits of B; because I is nonzero, B is a proper valuation subring, so TauCeti.Place.ofValuationSubring turns it into a place.

Zeros and poles

theorem TauCeti.Place.exists_ord_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) : ∃ (P : Place k F), 0 < P.ord x

Stichtenoth, Corollary 1.1.20. An element of an algebraic function field transcendental over the constants has a zero: some place at which its order is positive.

theorem TauCeti.Place.exists_ord_neg {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) : ∃ (P : Place k F), P.ord x < 0

Stichtenoth, Corollary 1.1.20. An element of an algebraic function field transcendental over the constants has a pole: some place at which its order is negative.

theorem TauCeti.Place.nonempty {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Nonempty (Place k F)

An algebraic function field has at least one place (Stichtenoth, Corollary 1.1.20).

theorem TauCeti.Place.infinite {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Infinite (Place k F)

An algebraic function field has infinitely many places (Stichtenoth, Corollary 1.3.2). Were there only finitely many, weak approximation would give a function with a simple zero at every place; having nonzero order somewhere, it would be transcendental over the constants, yet it would have no pole.

The constants are the everywhere-regular functions

theorem TauCeti.Place.mem_algebraicClosure_iff_forall_mem_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {f : F} : f ∈ algebraicClosure k F ↔ ∀ (P : Place k F), f ∈ P.integers

algebraicClosure k F = ⋂_P 𝒪_P (Stichtenoth, Corollary 1.1.20): an element of an algebraic function field is algebraic over the constants exactly when it has no pole.

theorem TauCeti.Place.coe_algebraicClosure_eq_iInter_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : ↑(algebraicClosure k F) = ⋂ (P : Place k F), ↑P.integers

algebraicClosure k F = ⋂_P 𝒪_P, as an equality of subsets of F (Stichtenoth, Corollary 1.1.20).

Places at infinity of affine models

theorem TauCeti.Place.exists_algebraMap_notMem_integers (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (R : Type w) [CommRing R] [Algebra R F] [IsFractionRing R F] (hF : IsFunctionField k F) : ∃ (P : Place k F) (r : R), (algebraMap R F) r ∉ P.integers

Every affine model of an algebraic function field has a place at infinity. If no place were infinite on R, every element of R would be regular at every place, hence algebraic over k (TauCeti.Place.mem_algebraicClosure_iff_forall_mem_integers); the algebraic elements form a subfield, so every fraction of two elements of R would be algebraic too, and F is the fraction field of R. That contradicts the transcendental element of an algebraic function field.