Valuation rings of an algebraic function field are the rings of places

Stichtenoth defines a valuation ring of F / k to be a subring 𝒪 with k ⊊ 𝒪 ⊊ F such that z ∈ 𝒪 or z⁻¹ ∈ 𝒪 for every z : F (Definition 1.1.4), and proves that every such ring is a discrete valuation ring (Theorem 1.1.6), so that the places of F / k are exactly the proper valuation subrings of F containing the constants (Theorem 1.1.13). This file proves that recognition theorem: TauCeti.Place.ofValuationSubring turns a proper ValuationSubring F containing k into a place whose valuation ring is the given one, and TauCeti.Place.existsUnique_integers_eq says the place is unique with that property.

The mathematical content is the discreteness, TauCeti.isDiscreteValuationRing_of_isFunctionField, and the argument is Stichtenoth's. The engine is Lemma 1.1.7: if x is a nonzero nonunit of 𝒪, then a family y i of nonunits whose valuations increase strictly and stay above v x is linearly independent over k(x), hence has at most [F : k(x)] members. Because x is transcendental — a nonunit cannot be algebraic over k — that degree is finite, so 𝒪 admits no infinite chain of nonunits of strictly increasing valuation. Two applications finish the proof: the valuations of the nonzero nonunits attain a maximum, at an element t, and every nonzero z : 𝒪 is t ^ n times a unit. That is exactly Mathlib's HasUnitMulPowIrreducibleFactorization.

Main results

• TauCeti.linearIndependent_of_strictMono_valuation: Stichtenoth, Lemma 1.1.7.
• TauCeti.isDiscreteValuationRing_of_isFunctionField: a proper valuation subring of an algebraic function field containing the constants is a discrete valuation ring (Stichtenoth, Theorem 1.1.6).
• TauCeti.Place.ofValuationSubring, with TauCeti.Place.valuation_ofValuationSubring and TauCeti.Place.integers_ofValuationSubring: the place attached to such a valuation subring, its valuation, and the fact that its valuation ring is the subring one started from.
• TauCeti.Place.existsUnique_integers_eq: the place is the unique one with that valuation ring (Stichtenoth, Theorem 1.1.13).

Implementation notes

Everything is phrased through ValuationSubring.valuation, the tautological valuation of a valuation subring, rather than through membership in the subring: x ∈ A is A.valuation x ≤ 1 and x is a nonunit of A exactly when A.valuation x < 1, and in this vocabulary the estimates of Lemma 1.1.7 are one-line applications of Valuation.map_sum_eq_of_lt. The value group of A.valuation is only known to be a linearly ordered commutative group with zero; that it is ℤᵐ⁰ is the conclusion, not a hypothesis, and it is obtained by handing the discrete valuation ring back to Mathlib's IsDiscreteValuationRing.maximalIdeal and the adic valuation of that height-one prime.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.1.6, Lemma 1.1.7 and Theorem 1.1.13.

Stichtenoth's chain estimate

theorem TauCeti.linearIndependent_of_strictMono_valuation {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hk : ∀ (c : k), (algebraMap k F) c ∈ A) {x : F} (hx0 : x ≠ 0) (hx : A.valuation x < 1) {ι : Type u_1} [LinearOrder ι] {y : ι → F} (hy : ∀ (i : ι), A.valuation (y i) < 1) (hmono : StrictMono fun (i : ι) => A.valuation (y i)) (hxy : ∀ (i : ι), A.valuation x ≤ A.valuation (y i)) : LinearIndependent (↥k⟮x⟯) y

Stichtenoth, Lemma 1.1.7. Let x be a nonzero nonunit of a valuation subring A of F containing the constants. A family of nonunits of A whose valuations increase strictly along a linear order, and are all at least A.valuation x — hence nonzero — is linearly independent over k(x).

In Stichtenoth's additive notation the hypothesis reads ord x ≥ ord (y i₀) > ord (y i₁) > ⋯ > 0, and the conclusion bounds the length of such a chain by [F : k(x)].

Discreteness

theorem TauCeti.isDiscreteValuationRing_of_isFunctionField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hF : IsFunctionField k F) (hk : ∀ (c : k), (algebraMap k F) c ∈ A) (hA : A ≠ ⊤) : IsDiscreteValuationRing ↥A

Stichtenoth, Theorem 1.1.6. A proper valuation subring of an algebraic function field that contains the constants is a discrete valuation ring.

The place of a valuation subring

theorem TauCeti.Place.valuationSubring_valuation_maximalIdeal {F : Type v} [Field F] (A : ValuationSubring F) [IsDiscreteValuationRing ↥A] : (IsDedekindDomain.HeightOneSpectrum.valuation F (IsDiscreteValuationRing.maximalIdeal ↥A)).valuationSubring = A

The valuation subring of the adic valuation of the maximal ideal of a discrete valuation subring A of F is A itself. This is Mathlib's IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, read through the fact that the structure map of a valuation subring is the inclusion.

noncomputable def TauCeti.Place.ofValuationSubring {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hF : IsFunctionField k F) (hk : ∀ (c : k), (algebraMap k F) c ∈ A) (hA : A ≠ ⊤) : Place k F

Stichtenoth, Theorem 1.1.13. The place of F / k attached to a proper valuation subring of F containing the constants: its valuation is the adic valuation of the maximal ideal of the subring, which is a discrete valuation ring by TauCeti.isDiscreteValuationRing_of_isFunctionField.

Equations

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

theorem TauCeti.Place.valuation_ofValuationSubring {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hF : IsFunctionField k F) (hk : ∀ (c : k), (algebraMap k F) c ∈ A) (hA : A ≠ ⊤) : (ofValuationSubring hF hk hA).valuation = have x := ⋯; IsDedekindDomain.HeightOneSpectrum.valuation F (IsDiscreteValuationRing.maximalIdeal ↥A)

The valuation of TauCeti.Place.ofValuationSubring is the adic valuation of the maximal ideal of the subring.

@[simp]

theorem TauCeti.Place.integers_ofValuationSubring {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hF : IsFunctionField k F) (hk : ∀ (c : k), (algebraMap k F) c ∈ A) (hA : A ≠ ⊤) : (ofValuationSubring hF hk hA).integers = A

The valuation ring of TauCeti.Place.ofValuationSubring is the subring one started from.

theorem TauCeti.Place.existsUnique_integers_eq {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hF : IsFunctionField k F) (hk : ∀ (c : k), (algebraMap k F) c ∈ A) (hA : A ≠ ⊤) : ∃! P : Place k F, P.integers = A

Stichtenoth, Theorem 1.1.13. A proper valuation subring of an algebraic function field containing the constants is the valuation ring of exactly one place.