The completed valuation ring at a rational place

Uniformizer expansion identifies the completed valuation ring at a rational place with k[[T]]. Every coefficient sequence is realized: its polynomial partial sums are Cauchy, and their limit has the prescribed finite expansions. The isomorphism sends a chosen uniformizer to T and identifies the order filtrations. With the constants discrete and power series given their coefficientwise topology, it is also a homeomorphism.

References

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

theorem TauCeti.Place.completionPlace_powerSeriesExpansion_surjective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) : Function.Surjective ⇑(P.completionPlace.powerSeriesExpansion ⋯ ⋯)

Every power series over the constants is the uniformizer expansion of an element of the completed valuation ring at a rational place.

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

Uniformizer expansion identifies the completed valuation ring at a rational place with the power-series ring over the constants.

Equations

• P.completionIntegersEquivPowerSeries hP ht = AlgEquiv.ofBijective (P.completionPlace.powerSeriesExpansion ⋯ ⋯) ⋯

theorem TauCeti.Place.completionIntegersEquivPowerSeries_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (x : ↥P.completionPlace.integers) : (P.completionIntegersEquivPowerSeries hP ht) x = (P.completionPlace.powerSeriesExpansion ⋯ ⋯) x

The completed-ring isomorphism is the uniformizer expansion map.

theorem TauCeti.Place.sub_sum_coeff_completionIntegersEquivPowerSeries_symm_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (f : PowerSeries k) (n : ℕ) : ↑((P.completionIntegersEquivPowerSeries hP ht).symm f) - ∑ i : Fin n, (algebraMap k P.Completion) ((PowerSeries.coeff ↑i) f) * P.completionEmbedding t ^ ↑i ∈ P.completionPlace.filtration ↑n

The inverse isomorphism realizes a power series to every finite order.

@[simp]

theorem TauCeti.Place.completionIntegersEquivPowerSeries_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) : (P.completionIntegersEquivPowerSeries hP ht) (P.completionIntegersEmbedding ⟨t, ⋯⟩) = PowerSeries.X

The chosen uniformizer maps to the power-series variable.

theorem TauCeti.Place.continuous_completionIntegersEquivPowerSeries {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) [TopologicalSpace k] [DiscreteTopology k] : Continuous ⇑(P.completionIntegersEquivPowerSeries hP ht)

Uniformizer expansion is continuous for the valuation topology on the completed ring and the coefficientwise topology on power series over the discrete constant field.

theorem TauCeti.Place.continuous_completionIntegersEquivPowerSeries_symm {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) [TopologicalSpace k] [DiscreteTopology k] : Continuous ⇑(P.completionIntegersEquivPowerSeries hP ht).symm

Realizing a power series in the completed valuation ring is continuous: agreement of finitely many coefficients gives approximation to any prescribed valuation precision.

noncomputable def TauCeti.Place.completionIntegersHomeomorphPowerSeries {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) [TopologicalSpace k] [DiscreteTopology k] : ↥P.completionPlace.integers ≃ₜ PowerSeries k

The completed valuation ring at a rational place is topologically k[[T]], with k discrete and the power-series ring carrying its coefficientwise topology.

Equations

• P.completionIntegersHomeomorphPowerSeries hP ht = { toEquiv := (P.completionIntegersEquivPowerSeries hP ht).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.Place.completionIntegersHomeomorphPowerSeries_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) [TopologicalSpace k] [DiscreteTopology k] (x : ↥P.completionPlace.integers) : (P.completionIntegersHomeomorphPowerSeries hP ht) x = (P.completionIntegersEquivPowerSeries hP ht) x

The topological identification uses the same uniformizer expansion as the algebraic one.

@[simp]

theorem TauCeti.Place.completionIntegersHomeomorphPowerSeries_symm_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) [TopologicalSpace k] [DiscreteTopology k] (f : PowerSeries k) : (P.completionIntegersHomeomorphPowerSeries hP ht).symm f = (P.completionIntegersEquivPowerSeries hP ht).symm f

The inverse topological identification is the inverse algebraic identification.