The completed valuation ring at a place is a power-series ring over the residue field

Let P be a place of F / k, let s : F_P → 𝒪̂_P be a coefficient field of the completed valuation ring, that is, a ring embedding of the residue field F_P lifting it, and let t be a uniformizer of the completion F̂_P. Then 𝒪̂_P is the power-series ring F_P[[T]]: every completed integral function has a unique expansion ∑ s(aᵢ) tⁱ with coefficients aᵢ ∈ F_P.

Coefficient fields exist at every place (TauCeti.Place.exists_completionResidueFieldSection), so 𝒪̂_P ≃ F_P[[T]] as rings at every place. When F_P is separable over k there is a unique coefficient field over k (TauCeti.Place.completionResidueFieldSection), and the expansion is a k-algebra isomorphism. When F_P is inseparable over k there may be no coefficient field over k, and then 𝒪̂_P is not k-isomorphic to F_P[[T]] at all (TauCeti.Place.isEmpty_completionIntegers_algEquiv_powerSeries); the ring isomorphism still exists, but it depends on the choice of the coefficient field.

This is the identification of a completed valuation ring with k[[T]] at a rational place (TauCeti.Place.completionIntegersEquivPowerSeries) carried over to places of arbitrary degree. The coefficients lie in F_P rather than k, which is what makes the t⁻¹-coefficient of a Laurent expansion, the residue at P, an element of F_P.

The proof views F̂_P as an F_P-algebra through the coefficient field. The completed place is then trivial on F_P, and its residue field is F_P itself, so it is a rational place over F_P. The uniformizer expansions at rational places (TauCeti.Place.powerSeriesExpansion) and the completeness of F̂_P (TauCeti.Place.powerSeriesExpansion_surjective) apply to it verbatim.

Main definitions

• TauCeti.Place.completionIntegersEquivPowerSeriesOfSection: the ring isomorphism 𝒪̂_P ≃ F_P[[T]] determined by a coefficient field s and a uniformizer t.
• TauCeti.Place.completionIntegersEquivPowerSeriesResidueField: the k-algebra isomorphism 𝒪̂_P ≃ₐ[k] F_P[[T]] at a place with separable residue field, through the coefficient field over k.

Main results

• TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_eq_iff: the expansion of x is the power series ∑ aᵢ Tⁱ exactly when x - ∑_{i < n} s(aᵢ) tⁱ vanishes to order n for every n.
• TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_section and TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_uniformizer: the coefficient field expands to the constant power series and t to T.
• TauCeti.Place.constantCoeff_completionIntegersEquivPowerSeriesOfSection: the constant coefficient is the value at P.
• TauCeti.Place.order_completionIntegersEquivPowerSeriesOfSection: the expansion preserves orders.
• TauCeti.Place.nonempty_completionIntegers_ringEquiv_powerSeries: at every place, separable residue field or not, 𝒪̂_P is isomorphic to F_P[[T]].

The same statements hold for the k-algebra isomorphism at a place with separable residue field, under the names with ResidueField in place of OfSection.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.2.
• J.-P. Serre, Local Fields, GTM 67, Springer, 1979, Chapter II, §4.

The completion as a rational place over a coefficient field

Power-series expansions over a coefficient field

noncomputable def TauCeti.Place.completionIntegersEquivPowerSeriesOfSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) : ↥P.completionPlace.integers ≃+* PowerSeries P.ResidueField

The completed valuation ring at a place is F_P[[T]]. Given a coefficient field s of 𝒪̂_P, a ring embedding of the residue field F_P lifting it, and a uniformizer t, the isomorphism sends a completed integral function to its expansion ∑ aᵢ Tⁱ in t, with coefficients aᵢ ∈ F_P read through s; it is characterized by TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_eq_iff.

theorem TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_eq_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) (f : PowerSeries P.ResidueField) : (P.completionIntegersEquivPowerSeriesOfSection s hs ht) x = f ↔ ∀ (n : ℕ), ↑x - ∑ i : Fin n, ↑(s ((PowerSeries.coeff ↑i) f)) * t ^ ↑i ∈ P.completionPlace.filtration ↑n

The expansion is characterized by its truncations: the expansion of x is the power series ∑ aᵢ Tⁱ exactly when x - ∑_{i < n} s(aᵢ) tⁱ vanishes to order n for every n.

theorem TauCeti.Place.sub_sum_coeff_completionIntegersEquivPowerSeriesOfSection_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) (n : ℕ) : ↑x - ∑ i : Fin n, ↑(s ((PowerSeries.coeff ↑i) ((P.completionIntegersEquivPowerSeriesOfSection s hs ht) x))) * t ^ ↑i ∈ P.completionPlace.filtration ↑n

Removing the first n terms of the expansion of a completed integral function leaves a function vanishing to order at least n.

theorem TauCeti.Place.sub_sum_coeff_completionIntegersEquivPowerSeriesOfSection_symm_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (f : PowerSeries P.ResidueField) (n : ℕ) : ↑((P.completionIntegersEquivPowerSeriesOfSection s hs ht).symm f) - ∑ i : Fin n, ↑(s ((PowerSeries.coeff ↑i) f)) * t ^ ↑i ∈ P.completionPlace.filtration ↑n

The inverse isomorphism realizes a power series over the residue field to every finite order.

@[simp]

theorem TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_section {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (a : P.ResidueField) : (P.completionIntegersEquivPowerSeriesOfSection s hs ht) (s a) = PowerSeries.C a

The coefficient field expands to the constant power series.

@[simp]

theorem TauCeti.Place.completionIntegersEquivPowerSeriesOfSection_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) : (P.completionIntegersEquivPowerSeriesOfSection s hs ht) ⟨t, ⋯⟩ = PowerSeries.X

The uniformizer expands as the power-series variable.

@[simp]

theorem TauCeti.Place.constantCoeff_completionIntegersEquivPowerSeriesOfSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) : PowerSeries.constantCoeff ((P.completionIntegersEquivPowerSeriesOfSection s hs ht) x) = P.residueFieldEquivCompletion.symm ((IsLocalRing.residue ↥P.completionPlace.integers) x)

The constant coefficient of the expansion is the value at P, read in F_P.

theorem TauCeti.Place.mem_filtration_iff_le_order_completionIntegersEquivPowerSeriesOfSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (n : ℕ) (x : ↥P.completionPlace.integers) : ↑x ∈ P.completionPlace.filtration ↑n ↔ ↑n ≤ ((P.completionIntegersEquivPowerSeriesOfSection s hs ht) x).order

Vanishing to order n is vanishing of the first n coefficients of the expansion.

theorem TauCeti.Place.order_completionIntegersEquivPowerSeriesOfSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) (hx : x ≠ 0) : ((P.completionIntegersEquivPowerSeriesOfSection s hs ht) x).order = ↑(P.completionPlace.ord ↑x).toNat

The order of a nonzero completed integral function is the first nonzero degree of its expansion.

theorem TauCeti.Place.nonempty_completionIntegers_ringEquiv_powerSeries {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Nonempty (↥P.completionPlace.integers ≃+* PowerSeries P.ResidueField)

At every place the completed valuation ring is F_P[[T]], separable residue field or not: a coefficient field exists by Cohen's theorem (TauCeti.Place.exists_completionResidueFieldSection) and a uniformizer exists because the valuation is normalized. When F_P is inseparable over k there may be no k-linear such isomorphism (TauCeti.Place.isEmpty_completionIntegers_algEquiv_powerSeries).

The k-linear expansion at a place with separable residue field

noncomputable def TauCeti.Place.completionIntegersEquivPowerSeriesResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) : ↥P.completionPlace.integers ≃ₐ[k] PowerSeries P.ResidueField

The completed valuation ring at a place with separable residue field is F_P[[T]] over k. The isomorphism sends a completed integral function to its expansion ∑ aᵢ Tⁱ in the uniformizer t, with coefficients aᵢ ∈ F_P read in the coefficient field TauCeti.Place.completionResidueFieldSection over k; it is TauCeti.Place.completionIntegersEquivPowerSeriesOfSection for that coefficient field.

theorem TauCeti.Place.completionIntegersEquivPowerSeriesResidueField_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) : (P.completionIntegersEquivPowerSeriesResidueField ht) x = (P.completionIntegersEquivPowerSeriesOfSection ↑P.completionResidueFieldSection ⋯ ht) x

The k-linear expansion is the expansion through the coefficient field over k.

theorem TauCeti.Place.completionIntegersEquivPowerSeriesResidueField_eq_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) (f : PowerSeries P.ResidueField) : (P.completionIntegersEquivPowerSeriesResidueField ht) x = f ↔ ∀ (n : ℕ), ↑x - ∑ i : Fin n, ↑(P.completionResidueFieldSection ((PowerSeries.coeff ↑i) f)) * t ^ ↑i ∈ P.completionPlace.filtration ↑n

The expansion is characterized by its truncations: the expansion of x is the power series ∑ aᵢ Tⁱ exactly when x - ∑_{i < n} aᵢ tⁱ vanishes to order n for every n, the coefficients aᵢ being read in the coefficient field.

theorem TauCeti.Place.sub_sum_coeff_completionIntegersEquivPowerSeriesResidueField_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) (n : ℕ) : ↑x - ∑ i : Fin n, ↑(P.completionResidueFieldSection ((PowerSeries.coeff ↑i) ((P.completionIntegersEquivPowerSeriesResidueField ht) x))) * t ^ ↑i ∈ P.completionPlace.filtration ↑n

Removing the first n terms of the expansion of a completed integral function leaves a function vanishing to order at least n.

theorem TauCeti.Place.sub_sum_coeff_completionIntegersEquivPowerSeriesResidueField_symm_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (f : PowerSeries P.ResidueField) (n : ℕ) : ↑((P.completionIntegersEquivPowerSeriesResidueField ht).symm f) - ∑ i : Fin n, ↑(P.completionResidueFieldSection ((PowerSeries.coeff ↑i) f)) * t ^ ↑i ∈ P.completionPlace.filtration ↑n

The inverse isomorphism realizes a power series over the residue field to every finite order.

@[simp]

theorem TauCeti.Place.completionIntegersEquivPowerSeriesResidueField_completionResidueFieldSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (a : P.ResidueField) : (P.completionIntegersEquivPowerSeriesResidueField ht) (P.completionResidueFieldSection a) = PowerSeries.C a

The coefficient field expands to the constant power series.

@[simp]

theorem TauCeti.Place.completionIntegersEquivPowerSeriesResidueField_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) : (P.completionIntegersEquivPowerSeriesResidueField ht) ⟨t, ⋯⟩ = PowerSeries.X

The uniformizer expands as the power-series variable.

@[simp]

theorem TauCeti.Place.constantCoeff_completionIntegersEquivPowerSeriesResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) : PowerSeries.constantCoeff ((P.completionIntegersEquivPowerSeriesResidueField ht) x) = P.residueFieldEquivCompletion.symm ((IsLocalRing.residue ↥P.completionPlace.integers) x)

The constant coefficient of the expansion is the value at P, read in F_P.

theorem TauCeti.Place.constantCoeff_completionIntegersEquivPowerSeriesResidueField_completionIntegersEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.integers) : PowerSeries.constantCoeff ((P.completionIntegersEquivPowerSeriesResidueField ht) (P.completionIntegersEmbedding x)) = (IsLocalRing.residue ↥P.integers) x

The constant coefficient of the expansion of a function regular at P is its value at P.

theorem TauCeti.Place.mem_filtration_iff_le_order_completionIntegersEquivPowerSeriesResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (n : ℕ) (x : ↥P.completionPlace.integers) : ↑x ∈ P.completionPlace.filtration ↑n ↔ ↑n ≤ ((P.completionIntegersEquivPowerSeriesResidueField ht) x).order

Vanishing to order n is vanishing of the first n coefficients of the expansion.

theorem TauCeti.Place.order_completionIntegersEquivPowerSeriesResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) (hx : x ≠ 0) : ((P.completionIntegersEquivPowerSeriesResidueField ht) x).order = ↑(P.completionPlace.ord ↑x).toNat

The order of a nonzero completed integral function is the first nonzero degree of its expansion.