Completion at a place

The completion of a field at a place carries the same normalized valuation and constant field embedding. Its valuation ring is a complete discrete valuation ring, and a uniformizer of the original field is still a uniformizer after completion.

The inclusion identifies every finite interval of the order filtration with the corresponding interval in the completion. In particular, completion does not change the residue field. These identifications allow local calculations with finitely many coefficients to pass between the field and its completion. No finiteness or perfectness of the residue field is assumed.

The underlying complete field and extension of the valuation are Mathlib's Valuation.Completion and Valued.valuedCompletion.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Section I.7.

@[reducible, inline]

abbrev TauCeti.Place.Completion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Type u_2

The completion of F for the valuation of P.

Equations

• P.Completion = P.valuation.Completion

@[instance_reducible]

noncomputable instance TauCeti.Place.instAlgebraCompletion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Algebra k P.Completion

The constants act on the completion through their embedding in F.

Equations

• P.instAlgebraCompletion = ((UniformSpace.Completion.coeRingHom.comp (WithVal.equiv P.valuation).symm.toRingHom).comp (algebraMap k F)).toAlgebra

noncomputable def TauCeti.Place.completionEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : F →ₐ[k] P.Completion

The canonical embedding of the field into its completion at P.

Equations

• P.completionEmbedding = { toRingHom := UniformSpace.Completion.coeRingHom.comp (WithVal.equiv P.valuation).symm.toRingHom, commutes' := ⋯ }

theorem TauCeti.Place.completionEmbedding_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : F) : P.completionEmbedding x = ↑(WithVal.toVal P.valuation x)

The canonical embedding is the uniform-space completion map on the valued field.

@[simp]

theorem TauCeti.Place.valuation_completionEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : F) : Valued.v (P.completionEmbedding x) = P.valuation x

The embedding into the completion preserves the normalized valuation.

theorem TauCeti.Place.denseRange_completionEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : DenseRange ⇑P.completionEmbedding

The original field is dense in its completion at P.

noncomputable def TauCeti.Place.completionPlace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Place k P.Completion

The extension of P to the completed field, with its original normalization.

Equations

• P.completionPlace = { valuation := Valued.v, valuation_surjective := ⋯, isTrivialOn := ⋯ }

@[simp]

theorem TauCeti.Place.completionPlace_valuation {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : P.Completion) : P.completionPlace.valuation x = Valued.v x

@[simp]

theorem TauCeti.Place.ord_completionEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : F) : P.completionPlace.ord (P.completionEmbedding x) = P.ord x

Completion preserves the order of every function, including the junk value at zero.

theorem TauCeti.Place.isUniformizer_completionEmbedding_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : F) : P.completionPlace.valuation.IsUniformizer (P.completionEmbedding x) ↔ P.valuation.IsUniformizer x

A uniformizer in the original field remains a uniformizer in the completion.

theorem TauCeti.Place.completionEmbedding_mem_filtration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a : ℤ} {x : F} : P.completionEmbedding x ∈ P.completionPlace.filtration a ↔ x ∈ P.filtration a

The embedding preserves every step of the order filtration.

instance TauCeti.Place.completeSpace_completionIntegers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : CompleteSpace ↥P.completionPlace.integers

The valuation ring of the completed field is complete for the induced uniform structure.

theorem TauCeti.Place.exists_sub_completionEmbedding_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : P.Completion) (b : ℤ) : ∃ (y : F), x - P.completionEmbedding y ∈ P.completionPlace.filtration b

A completed function can be approximated by a function in F to any prescribed order.

theorem TauCeti.Place.exists_filtration_sub_completionEmbedding_mem {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a b : ℤ} (hab : a ≤ b) (x : ↥(P.completionPlace.filtration a)) : ∃ (y : ↥(P.filtration a)), ↑x - P.completionEmbedding ↑y ∈ P.completionPlace.filtration b

An element of the completed filtration has an approximation in the original filtration, with error in any smaller step.

noncomputable def TauCeti.Place.completionFiltrationMap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (a : ℤ) : ↥(P.filtration a) →ₗ[k] ↥(P.completionPlace.filtration a)

The inclusion of a step of the order filtration into its completed counterpart.

Equations

• P.completionFiltrationMap a = LinearMap.codRestrict (P.completionPlace.filtration a) (P.completionEmbedding.toLinearMap.domRestrict (P.filtration a)) ⋯

@[simp]

theorem TauCeti.Place.completionFiltrationMap_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (a : ℤ) (x : ↥(P.filtration a)) : ↑((P.completionFiltrationMap a) x) = P.completionEmbedding ↑x

noncomputable def TauCeti.Place.completionFiltrationQuotientEquiv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a b : ℤ} (hab : a ≤ b) : (↥(P.filtration a) ⧸ (P.filtration b).submoduleOf (P.filtration a)) ≃ₗ[k] ↥(P.completionPlace.filtration a) ⧸ (P.completionPlace.filtration b).submoduleOf (P.completionPlace.filtration a)

Completion preserves every finite interval of the order filtration. The isomorphism is induced by the canonical embedding, rather than by choices of representatives.

Equations

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

@[simp]

theorem TauCeti.Place.completionFiltrationQuotientEquiv_apply_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a b : ℤ} (hab : a ≤ b) (x : ↥(P.filtration a)) : (P.completionFiltrationQuotientEquiv hab) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((P.completionFiltrationMap a) x)

The filtration quotient equivalence sends the class of a function to the class of its canonical image in the completion.

noncomputable def TauCeti.Place.completionIntegersEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : ↥P.integers →ₐ[k] ↥P.completionPlace.integers

The canonical map of valuation rings induced by completion.

Equations

• P.completionIntegersEmbedding = { toFun := fun (x : ↥P.integers) => ⟨P.completionEmbedding ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem TauCeti.Place.completionIntegersEmbedding_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : ↥P.integers) : ↑(P.completionIntegersEmbedding x) = P.completionEmbedding ↑x

instance TauCeti.Place.isLocalHom_completionIntegersEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : IsLocalHom P.completionIntegersEmbedding

Completion reflects units of the valuation ring.

noncomputable def TauCeti.Place.residueFieldEquivCompletion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.ResidueField ≃ₐ[k] P.completionPlace.ResidueField

Completion induces an isomorphism of residue fields over the original constants.

Equations

• P.residueFieldEquivCompletion = AlgEquiv.ofBijective (IsLocalRing.ResidueField.mapAlgHom P.completionIntegersEmbedding) ⋯

@[simp]

theorem TauCeti.Place.residueFieldEquivCompletion_apply_residue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : ↥P.integers) : P.residueFieldEquivCompletion ((IsLocalRing.residue ↥P.integers) x) = (IsLocalRing.residue ↥P.completionPlace.integers) (P.completionIntegersEmbedding x)

The residue-field isomorphism commutes with reduction of integral functions.

@[simp]

theorem TauCeti.Place.degree_completionPlace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.completionPlace.degree = P.degree

Completing a place preserves its degree over the constants.