Places of an algebraic function field

A place of a field extension F/k is a normalized discrete valuation of F that is trivial on k: a valuation v : Valuation F ℤᵐ⁰ which is surjective and satisfies v c = 1 for every nonzero constant c. This is the object Stichtenoth introduces in Algebraic Function Fields and Codes, Definitions 1.1.4 and 1.1.9, presented here in the normalized form: because the value group is pinned to be all of ℤᵐ⁰, no quotient by valuation equivalence is needed and equality of places is equality of valuations (TauCeti.Place.eq_of_isEquiv).

Main definitions

• TauCeti.Place k F: a place of F/k.
• TauCeti.Place.integers: the valuation ring 𝒪_P ⊆ F of a place.
• TauCeti.Place.ord: the additive order function ord_P : F → ℤ, normalized so that a prime element has order 1. It has the junk value ord_P 0 = 0.
• TauCeti.Place.ResidueField: the residue field F_P = 𝒪_P / 𝔪_P, a k-algebra.
• TauCeti.Place.degree: the degree deg P = [F_P : k] of a place.
• TauCeti.Place.ordAddMonoidHom: ord_P bundled as an additive homomorphism on Additive Fˣ. Restricting to units is what makes it additive, since ord_P 0 = 0 is a junk value.
• TauCeti.Place.ord_mul_eq_zero, ord_inv_eq_zero and ord_div_eq_zero: the units of order zero form a subgroup of Fˣ, read off that homomorphism. Its identity is ord_one itself, since ((1 : Fˣ) : F) is 1 definitionally.

Main results

• TauCeti.Place.instIsDiscreteValuationRing: 𝒪_P is a discrete valuation ring (Stichtenoth, Theorem 1.1.6), with TauCeti.Place.isUniformizer_iff_ord_eq_one identifying Mathlib's uniformizers as the elements of order one — Stichtenoth's prime elements — and TauCeti.Place.exists_eq_zpow_mul_unit writing every nonzero f : F as t ^ (ord_P f) times a unit of 𝒪_P.
• TauCeti.Place.ord_add_eq_min_of_ord_ne: the strict triangle inequality (Stichtenoth, Lemma 1.1.11).
• TauCeti.Place.valuation_eq_one_of_isAlgebraic: every nonzero element that is algebraic over k is a unit of 𝒪_P; equivalently, an element of nonzero order is transcendental over k (TauCeti.Place.transcendental_of_ord_ne_zero). In particular the constant field algebraicClosure k F is contained in 𝒪_P (TauCeti.Place.mem_integers_of_mem_algebraicClosure).
• TauCeti.Place.integers_injective: a place is determined by its valuation ring (Stichtenoth, Theorem 1.1.13), and TauCeti.Place.eq_of_integers_le: the valuation ring of a place is a maximal proper subring of F, so a place whose valuation ring contains that of another place is that place (Stichtenoth, Theorem 1.1.13(d)).
• TauCeti.Place.mem_integers_of_isIntegral: the valuation ring of a place is integrally closed in F.
• TauCeti.Place.degree_eq_one_iff_algebraMap_surjective and TauCeti.Place.degree_eq_one_iff_forall_exists_valuation_sub_lt_one: the rational places are those whose residue field is exhausted by the constants, equivalently those at which every integral function agrees with a constant to first order; TauCeti.Place.residueFieldEquivOfDegreeEqOne identifies the residue field of such a place with k.

Implementation notes

Mathlib's multiplicative convention is used throughout: 𝒪_P is {f | v_P f ≤ 1} and a prime element t has v_P t = WithZero.exp (-1), so that ord_P t = 1. The translation between the two views is TauCeti.Place.valuation_eq_exp_neg_ord. Because WithZero.log 0 = 0, the order function has the junk value ord_P 0 = 0; statements about ord_P f therefore carry f ≠ 0 whenever the junk value would falsify them, and the junk-free multiplicative form is stated alongside where both are useful.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.1.

structure TauCeti.Place (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] : Type v

A place of the field extension F/k is a normalized discrete valuation of F that is trivial on the constants: a ℤᵐ⁰-valued valuation which is surjective — so that its value group is exactly ℤ — and which takes the value 1 on every nonzero element of k.

Normalization removes the need to quotient by valuation equivalence: two places are equal as soon as their valuations are equivalent (TauCeti.Place.eq_of_isEquiv).

• valuation : Valuation F (WithZero (Multiplicative ℤ))

  The normalized valuation of the place. Following Mathlib's multiplicative convention, the elements of the valuation ring are those with valuation f ≤ 1, and a prime element t satisfies valuation t = WithZero.exp (-1).

• valuation_surjective : Function.Surjective ⇑self.valuation

  The valuation is surjective, i.e. normalized: its value group is all of ℤᵐ⁰.

• isTrivialOn : Valuation.IsTrivialOn k self.valuation

  The valuation is trivial on the constants.

instance TauCeti.Place.instIsTrivialOnWithZeroMultiplicativeIntValuation {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Valuation.IsTrivialOn k P.valuation

theorem TauCeti.Place.ext {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P Q : Place k F} (h : P.valuation = Q.valuation) : P = Q

theorem TauCeti.Place.ext_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P Q : Place k F} : P = Q ↔ P.valuation = Q.valuation

theorem TauCeti.Place.valuation_injective {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : Function.Injective valuation

def TauCeti.Place.integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : ValuationSubring F

The valuation ring 𝒪_P = {f : F | v_P f ≤ 1} of a place (Stichtenoth, Definition 1.1.4).

Equations

• P.integers = P.valuation.valuationSubring

theorem TauCeti.Place.integers_def {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.integers = P.valuation.valuationSubring

The defining equation of Place.integers: the valuation ring of a place is Mathlib's valuation subring of its underlying valuation. The body of Place.integers is not exposed to importing modules, so this is how generic valuation-subring constructions are transported to it.

@[simp]

theorem TauCeti.Place.mem_integers_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} : f ∈ P.integers ↔ P.valuation f ≤ 1

noncomputable def TauCeti.Place.ord {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : F) : ℤ

The additive order function ord_P : F → ℤ of a place, normalized so that a prime element has order 1. It has the junk value ord_P 0 = 0.

Equations

• P.ord f = P.valuation.ord f

theorem TauCeti.Place.ord_def {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : F) : P.ord f = -(P.valuation f).log

theorem TauCeti.Place.valuation_eq_exp_neg_ord {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : f ≠ 0) : P.valuation f = WithZero.exp (-P.ord f)

The translation between the multiplicative and additive views of a place.

theorem TauCeti.Place.ord_eq_iff_valuation_eq_exp_neg {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : f ≠ 0) {n : ℤ} : P.ord f = n ↔ P.valuation f = WithZero.exp (-n)

@[simp]

theorem TauCeti.Place.ord_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.ord 0 = 0

@[simp]

theorem TauCeti.Place.ord_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.ord 1 = 0

theorem TauCeti.Place.ord_mul {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) : P.ord (f * g) = P.ord f + P.ord g

theorem TauCeti.Place.ord_prod {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {ι : Type u_1} (s : Finset ι) {f : ι → F} (hf : ∀ i ∈ s, f i ≠ 0) : P.ord (∏ i ∈ s, f i) = ∑ i ∈ s, P.ord (f i)

@[simp]

theorem TauCeti.Place.ord_inv {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : F) : P.ord f⁻¹ = -P.ord f

@[simp]

theorem TauCeti.Place.ord_zpow {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : F) (n : ℤ) : P.ord (f ^ n) = n * P.ord f

@[simp]

theorem TauCeti.Place.ord_pow {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : F) (n : ℕ) : P.ord (f ^ n) = ↑n * P.ord f

theorem TauCeti.Place.ord_div {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) : P.ord (f / g) = P.ord f - P.ord g

noncomputable def TauCeti.Place.ordAddMonoidHom {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Additive Fˣ →+ ℤ

The order of vanishing at a place, as a homomorphism out of the additivized group of units Additive Fˣ. Restricting to units is what makes it additive: ord_P is only additive away from the junk value ord_P 0 = 0.

Equations

• P.ordAddMonoidHom = AddMonoidHom.mk' (fun (z : Additive Fˣ) => P.ord ↑(Additive.toMul z)) ⋯

@[simp]

theorem TauCeti.Place.ordAddMonoidHom_apply {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (z : Fˣ) : P.ordAddMonoidHom (Additive.ofMul z) = P.ord ↑z

theorem TauCeti.Place.ord_mul_eq_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.ord ↑(f * g) = 0

A product of order-zero units has order zero.

theorem TauCeti.Place.ord_inv_eq_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) : P.ord ↑f⁻¹ = 0

The inverse of an order-zero unit has order zero.

theorem TauCeti.Place.ord_zpow_eq_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) (n : ℤ) : P.ord ↑(f ^ n) = 0

A power of an order-zero unit has order zero.

theorem TauCeti.Place.ord_div_eq_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.ord ↑(f / g) = 0

A quotient of order-zero units has order zero.

@[simp]

theorem TauCeti.Place.ord_neg {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : F) : P.ord (-f) = P.ord f

theorem TauCeti.Place.ord_div_zpow {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f t : F} (hf : f ≠ 0) (ht : t ≠ 0) (n : ℤ) : P.ord (f / t ^ n) = P.ord f - n * P.ord t

The order of a quotient by an integral power.

theorem TauCeti.Place.ord_surjective {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Function.Surjective P.ord

theorem TauCeti.Place.exists_ne_zero_ord_eq {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℤ) : ∃ (t : F), t ≠ 0 ∧ P.ord t = n

Every integer is the order of a nonzero function: the sharpening of TauCeti.Place.ord_surjective that the junk value ord_P 0 = 0 makes necessary, since the element ord_surjective produces at 0 may itself be 0.

theorem TauCeti.Place.mem_integers_iff_ord_nonneg {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} : f ∈ P.integers ↔ 0 ≤ P.ord f

theorem TauCeti.Place.min_ord_le_ord_add {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f g : F} (h : f + g ≠ 0) : min (P.ord f) (P.ord g) ≤ P.ord (f + g)

The ultrametric inequality, in additive form. The hypothesis f + g ≠ 0 guards the junk value ord_P 0 = 0.

theorem TauCeti.Place.ord_add_eq_min_of_ord_ne {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (h : P.ord f ≠ P.ord g) : P.ord (f + g) = min (P.ord f) (P.ord g)

The strict triangle inequality (Stichtenoth, Lemma 1.1.11): if two nonzero elements have distinct orders, the order of their sum is the smaller of the two.

theorem TauCeti.Place.sum_ne_zero_of_forall_ord_lt {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {ι : Type u_1} {s : Finset ι} {f : ι → F} {j : ι} (hj : j ∈ s) (hfj : f j ≠ 0) (hlt : ∀ i ∈ s, i ≠ j → P.ord (f j) < P.ord (f i)) : ∑ i ∈ s, f i ≠ 0

A finite sum one of whose summands has strictly least order at P does not vanish.

theorem TauCeti.Place.ord_sum_eq_of_forall_lt {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {ι : Type u_1} {s : Finset ι} {f : ι → F} {j : ι} (hj : j ∈ s) (hfj : f j ≠ 0) (hlt : ∀ i ∈ s, i ≠ j → P.ord (f j) < P.ord (f i)) : P.ord (∑ i ∈ s, f i) = P.ord (f j)

The strict triangle inequality for a finite sum: a summand of strictly least order at P dictates the order of the sum.

theorem TauCeti.Place.linearIndependent_of_injective_ord {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {ι : Type u_1} {f : ι → F} (hf : ∀ (i : ι), f i ≠ 0) (hinj : Function.Injective fun (i : ι) => P.ord (f i)) : LinearIndependent k f

Functions of pairwise distinct orders are linearly independent over the constants: a family of nonzero functions whose orders at P are pairwise distinct is k-linearly independent, because the summand of least order dictates the order of any nontrivial linear combination.

theorem TauCeti.Place.exists_ne_zero_forall_div_mem_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {ι : Type u_1} [Finite ι] (c : ι → F) {i₁ : ι} (hi₁ : c i₁ ≠ 0) : ∃ (i₀ : ι), c i₀ ≠ 0 ∧ ∀ (i : ι), c i / c i₀ ∈ P.integers

Normalizing a family of coefficients. A finite family in F that does not vanish identically has a nonzero member by which the whole family can be divided without leaving 𝒪_P; a member of least order at P is one. This is what turns a relation with coefficients in F into a relation with coefficients in 𝒪_P, one of which is a unit.

@[simp]

theorem TauCeti.Place.ord_algebraMap {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (c : k) : P.ord ((algebraMap k F) c) = 0

theorem TauCeti.Place.algebraMap_mem_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (c : k) : (algebraMap k F) c ∈ P.integers

theorem TauCeti.Place.valuation_eq_one_of_isAlgebraic {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : IsAlgebraic k f) (hf0 : f ≠ 0) : P.valuation f = 1

Every nonzero element algebraic over the constants has valuation one. This is the contrapositive of Mathlib's Valuation.transcendental_of_ne_one.

theorem TauCeti.Place.ord_eq_zero_of_isAlgebraic {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : IsAlgebraic k f) : P.ord f = 0

Elements algebraic over the constants have order zero at every place.

theorem TauCeti.Place.transcendental_of_ord_ne_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : P.ord f ≠ 0) : Transcendental k f

An element of nonzero order is transcendental over the constants.

theorem TauCeti.Place.mem_integers_of_mem_algebraicClosure {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : f ∈ algebraicClosure k F) : f ∈ P.integers

The constant field algebraicClosure k F is contained in the valuation ring of every place: constants are everywhere regular.

theorem TauCeti.Place.valueGroup_eq_top {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : (↑P.valuation).valueGroup = ⊤

Normalization says exactly that the value group of a place is all of ℤᵐ⁰.

instance TauCeti.Place.instNontrivialSubtypeUnitsWithZeroMultiplicativeIntMemSubgroupValueGroupValuation {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Nontrivial ↥(↑P.valuation).valueGroup

instance TauCeti.Place.instIsDiscreteValuationRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : IsDiscreteValuationRing ↥P.integers

The valuation ring of a place is a discrete valuation ring (Stichtenoth, Theorem 1.1.6).

theorem TauCeti.Place.generator_eq_exp_neg_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Valuation.IsRankOneDiscrete.generator P.valuation = Units.mk0 (WithZero.exp (-1)) generator_eq_exp_neg_one._proof_1

The generator of the value group singled out by Mathlib's discreteness API is WithZero.exp (-1), because the valuation of a place is normalized.

@[simp]

theorem TauCeti.Place.isUniformizer_iff_ord_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} : P.valuation.IsUniformizer t ↔ P.ord t = 1

Mathlib's uniformizers of v_P are exactly the elements of order one: Stichtenoth's prime elements for P.

theorem TauCeti.Place.exists_isUniformizer {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : ∃ (t : F), P.valuation.IsUniformizer t

theorem TauCeti.Place.isUnit_iff_valuation_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {x : ↥P.integers} : IsUnit x ↔ P.valuation ↑x = 1

theorem TauCeti.Place.isUnit_iff_ord_eq_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {x : ↥P.integers} (hx : ↑x ≠ 0) : IsUnit x ↔ P.ord ↑x = 0

theorem TauCeti.Place.exists_eq_zpow_mul_unit {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (ht : P.valuation.IsUniformizer t) {f : F} (hf : f ≠ 0) : ∃ (u : (↥P.integers)ˣ), f = t ^ P.ord f * ↑↑u

Existence half of Stichtenoth, Theorem 1.1.6(b): relative to a prime element t for P, every nonzero f : F is t ^ (ord_P f) times a unit of 𝒪_P.

theorem TauCeti.Place.mem_maximalIdeal_iff_valuation_lt_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : ↥P.integers} : f ∈ IsLocalRing.maximalIdeal ↥P.integers ↔ P.valuation ↑f < 1

theorem TauCeti.Place.valuation_lt_one_iff_ord_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : F} (hf : f ≠ 0) : P.valuation f < 1 ↔ 0 < P.ord f

The elements of positive order are exactly those of valuation less than one: the maximal ideal of 𝒪_P, read at the level of F.

theorem TauCeti.Place.mem_maximalIdeal_iff_ord_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : ↥P.integers} (hf : ↑f ≠ 0) : f ∈ IsLocalRing.maximalIdeal ↥P.integers ↔ 0 < P.ord ↑f

theorem TauCeti.Place.integers_ne_top {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.integers ≠ ⊤

The valuation ring of a place is a proper subring of F (Stichtenoth, Definition 1.1.4).

theorem TauCeti.Place.eq_of_isEquiv {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P Q : Place k F} (h : P.valuation.IsEquiv Q.valuation) : P = Q

A place is determined by its valuation: two places whose valuations are equivalent are equal. This is the payoff of normalizing the value group, and half of Stichtenoth's Theorem 1.1.13.

@[simp]

theorem TauCeti.Place.valuation_isEquiv_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P Q : Place k F} : P.valuation.IsEquiv Q.valuation ↔ P = Q

theorem TauCeti.Place.integers_injective {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : Function.Injective integers

A place is determined by its valuation ring (Stichtenoth, Theorem 1.1.13).

theorem TauCeti.Place.eq_of_integers_le {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P Q : Place k F} (h : P.integers ≤ Q.integers) : P = Q

The valuation ring of a place is a maximal proper subring of F (Stichtenoth, Theorem 1.1.13(d)), in the form used to recognize a place from a containment of valuation rings: a place whose valuation ring contains the valuation ring of another place is that place.

This is Mathlib's ValuationSubring.eq_of_le_of_ne_top for 𝒪_P, which applies because a discrete valuation ring has Krull dimension at most one; properness of 𝒪_Q is what rules out the other case.

theorem TauCeti.Place.mem_integers_of_isIntegral {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {R : Type u_1} [CommRing R] [Algebra R F] (hR : ∀ (r : R), (algebraMap R F) r ∈ P.integers) {y : F} (hy : IsIntegral R y) : y ∈ P.integers

The valuation ring of a place is integrally closed in F: an element of F integral over a k-algebra whose image lies in 𝒪_P lies in 𝒪_P.

@[instance_reducible]

noncomputable instance TauCeti.Place.instAlgebraSubtypeMemValuationSubringIntegers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Algebra k ↥P.integers

Constants are integral at every place, so 𝒪_P is a k-algebra.

Equations

• P.instAlgebraSubtypeMemValuationSubringIntegers = ((algebraMap k F).codRestrict P.integers ⋯).toAlgebra

instance TauCeti.Place.instIsScalarTowerSubtypeMemValuationSubringIntegers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : IsScalarTower k (↥P.integers) F

@[simp]

theorem TauCeti.Place.coe_algebraMap_constants {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (c : k) : ↑((algebraMap k ↥P.integers) c) = (algebraMap k F) c

A constant, viewed in 𝒪_P and then back in F, is that constant. The name says constants rather than integers because TauCeti.Place.coe_algebraMap_integers is the corresponding statement for the algebra map between the valuation rings of two places.

@[reducible, inline]

noncomputable abbrev TauCeti.Place.ResidueField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : Type v

The residue field F_P = 𝒪_P / 𝔪_P of a place (Stichtenoth, Definition 1.1.14). The evaluation map f ↦ f(P) is IsLocalRing.residue P.integers.

Equations

• P.ResidueField = IsLocalRing.ResidueField ↥P.integers

theorem TauCeti.Place.algebraMap_residueField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {R : Type u_1} [CommSemiring R] [Algebra R ↥P.integers] [Algebra R P.ResidueField] [IsScalarTower R (↥P.integers) P.ResidueField] (r : R) : (algebraMap R P.ResidueField) r = (IsLocalRing.residue ↥P.integers) ((algebraMap R ↥P.integers) r)

The canonical map from an algebra acting compatibly on the valuation ring to the residue field is reduction after the map to the valuation ring.

theorem TauCeti.Place.residue_eq_zero_iff_valuation_lt_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : ↥P.integers} : (IsLocalRing.residue ↥P.integers) f = 0 ↔ P.valuation ↑f < 1

Evaluation at a place vanishes exactly on elements of positive valuation.

theorem TauCeti.Place.residue_eq_zero_iff_ord_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {f : ↥P.integers} (hf : ↑f ≠ 0) : (IsLocalRing.residue ↥P.integers) f = 0 ↔ 0 < P.ord ↑f

Evaluation at a place vanishes on a nonzero function exactly when that function has positive order: the additive form of TauCeti.Place.residue_eq_zero_iff_valuation_lt_one.

noncomputable def TauCeti.Place.degree {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : ℕ

The degree deg P = [F_P : k] of a place (Stichtenoth, Definition 1.1.14). Its finiteness, which guards the junk value of Module.finrank, holds whenever F/k is a function field: see TauCeti.Place.finiteDimensional_residueField (Stichtenoth, Proposition 1.1.15).

Equations

• P.degree = Module.finrank k P.ResidueField

theorem TauCeti.Place.degree_eq_finrank {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.degree = Module.finrank k P.ResidueField

theorem TauCeti.Place.one_le_degree {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) [Module.Finite k P.ResidueField] : 1 ≤ P.degree

theorem TauCeti.Place.degree_eq_one_iff_algebraMap_surjective {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.degree = 1 ↔ Function.Surjective ⇑(algebraMap k P.ResidueField)

A place has degree one exactly when every residue is the residue of a constant: the rational places (Stichtenoth, Definition 1.1.14).

theorem TauCeti.Place.degree_eq_one_iff_forall_exists_valuation_sub_lt_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.degree = 1 ↔ ∀ f ∈ P.integers, ∃ (c : k), P.valuation (f - (algebraMap k F) c) < 1

A place is rational exactly when every function integral at P agrees with a constant to first order: this is the sense in which the value f(P) of a function at a rational place is an element of k. The multiplicative form avoids the junk value ord_P 0 = 0, which occurs here whenever f is itself a constant.

noncomputable def TauCeti.Place.residueFieldEquivOfDegreeEqOne {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (h : P.degree = 1) : k ≃ₐ[k] P.ResidueField

A rational place has residue field k: at a place of degree one the constants map isomorphically onto the residue field, so f(P) really is an element of k.

Equations

• P.residueFieldEquivOfDegreeEqOne h = AlgEquiv.ofBijective (Algebra.ofId k P.ResidueField) ⋯

@[simp]

theorem TauCeti.Place.residueFieldEquivOfDegreeEqOne_apply {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (h : P.degree = 1) (c : k) : (P.residueFieldEquivOfDegreeEqOne h) c = (algebraMap k P.ResidueField) c

theorem TauCeti.Place.degree_eq_one_of_isAlgClosed_of_isIntegral {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) [IsAlgClosed k] [Algebra.IsIntegral k P.ResidueField] : P.degree = 1

If the residue field of a place is algebraic over an algebraically closed field of constants, then the place is rational (Stichtenoth, Remark 1.1.17).