The coefficient field of the completion at a place

Let P be a place of F / k whose residue field F_P is separable over k; over a perfect constant field this holds at every place with finite residue field, in particular at every place of an algebraic function field. The completed valuation ring 𝒪̂_P is complete for the adic topology of its maximal ideal (TauCeti.Place.isAdicComplete_completionIntegers), so it contains a unique copy of F_P over k mapping onto the residue field: a k-algebra embedding F_P → 𝒪̂_P which reduces to the identity of F_P.

At a rational place this embedding is just the constant field k, and expansions in a uniformizer t have coefficients in k. At a place of higher degree the coefficients of the P-adic expansion ∑ aᵢ tⁱ of a completed function are taken in the image of this embedding, which is what makes them, and the residue a₋₁, elements of F_P.

Without separability 𝒪̂_P still has a coefficient field, by Cohen's theorem for complete local rings containing a field, but it is only linear over the prime field: there may be no k-algebra embedding of F_P into 𝒪̂_P at all.

Main definitions

• TauCeti.Place.completionResidueFieldSection: the coefficient field F_P →ₐ[k] 𝒪̂_P.

Main results

• TauCeti.Place.residue_completionResidueFieldSection: it reduces to the identification of F_P with the residue field of the completion.
• TauCeti.Place.eq_completionResidueFieldSection: it is the only k-algebra embedding of F_P with this property.
• TauCeti.Place.sub_completionResidueFieldSection_mem_filtration_one and TauCeti.Place.completionEmbedding_sub_completionResidueFieldSection_mem_filtration_one: every integral completed function, in particular every function regular at P, agrees with the coefficient-field lift of its value at P up to a function vanishing at P.
• TauCeti.Place.exists_completionResidueFieldSection: at every place, separable residue field or not, 𝒪̂_P has a coefficient field, in general not k-linear.

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.

theorem TauCeti.Place.exists_completionResidueFieldSection {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), ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a

The completion at any place has a coefficient field: a ring embedding of the residue field F_P into the completed valuation ring 𝒪̂_P which reduces to the identification of F_P with the residue field of the completion. No separability of F_P over k is assumed (Cohen's theorem, TauCeti.exists_residueFieldSection). When F_P / k is separable, TauCeti.Place.completionResidueFieldSection is a k-linear one. Otherwise there may be no k-linear one (TauCeti.Place.isEmpty_algHom_residueField_completion).

instance TauCeti.Place.isSeparable_completionPlace_residueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] : Algebra.IsSeparable k P.completionPlace.ResidueField

Completion does not change the residue field, so it preserves its separability over the constants.

instance TauCeti.Place.formallyEtale_completionPlace_residueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] : Algebra.FormallyEtale k P.completionPlace.ResidueField

The residue field of the completion is formally étale over the constants, being separable; this is the hypothesis under which TauCeti.residueFieldSection exists and is unique.

noncomputable def TauCeti.Place.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] : P.ResidueField →ₐ[k] ↥P.completionPlace.integers

The coefficient field of the completion at a place with separable residue field: the unique k-algebra embedding of the residue field F_P into the completed valuation ring whose reduction is the identification TauCeti.Place.residueFieldEquivCompletion of F_P with the residue field of the completion.

theorem TauCeti.Place.completionResidueFieldSection_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] (a : P.ResidueField) : P.completionResidueFieldSection a = (residueFieldSection k ↥P.completionPlace.integers) (P.residueFieldEquivCompletion a)

The coefficient field of the completion at P is the coefficient field of the complete local ring 𝒪̂_P, read through the identification of the residue fields.

@[simp]

theorem TauCeti.Place.residue_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] (a : P.ResidueField) : (IsLocalRing.residue ↥P.completionPlace.integers) (P.completionResidueFieldSection a) = P.residueFieldEquivCompletion a

The coefficient field reduces to the identification of the residue fields.

theorem TauCeti.Place.eq_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] {s : P.ResidueField →ₐ[k] ↥P.completionPlace.integers} (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) : s = P.completionResidueFieldSection

The coefficient field is the only k-algebra embedding of the residue field into the completed valuation ring which reduces to the identification of the residue fields.

theorem TauCeti.Place.sub_completionResidueFieldSection_mem_filtration_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] (x : ↥P.completionPlace.integers) : ↑x - ↑(P.completionResidueFieldSection (P.residueFieldEquivCompletion.symm ((IsLocalRing.residue ↥P.completionPlace.integers) x))) ∈ P.completionPlace.filtration 1

An integral completed function agrees with the coefficient-field lift of its value at P up to a completed function vanishing at P.

theorem TauCeti.Place.completionEmbedding_sub_completionResidueFieldSection_mem_filtration_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] (x : ↥P.integers) : P.completionEmbedding ↑x - ↑(P.completionResidueFieldSection ((IsLocalRing.residue ↥P.integers) x)) ∈ P.completionPlace.filtration 1

A function regular at P agrees, in the completion, with the coefficient-field lift of its value at P up to a completed function vanishing at P.