No coefficient field over the constants at an inseparable residue field

At a place P of F / k whose residue field F_P is separable over k, the completed valuation ring 𝒪̂_P contains a unique copy of F_P over k lifting the residue field (TauCeti.Place.completionResidueFieldSection), and a uniformizer identifies 𝒪̂_P with F_P[[T]] and the completion F̂_P with F_P((T)) over k (TauCeti.Place.completionIntegersEquivPowerSeriesResidueField, TauCeti.Place.completionEquivLaurentSeriesResidueField). This file shows that the separability hypothesis of these constructions cannot be dropped.

Let k have characteristic p, let c ∈ k, and let z ∈ F be such that z ^ p - c has positive order at P, not divisible by p. Then the value z(P) is a p-th root of c in F_P, but c has no p-th root in F̂_P: if b ^ p = c, then z ^ p - c = (z - b) ^ p would have order divisible by p. So there is no k-algebra map F_P → F̂_P at all, and in particular no coefficient field over k and no k-linear identification of 𝒪̂_P with F_P[[T]] or of F̂_P with F_P((T)); the residue field F_P is inseparable over k.

The hypotheses hold over every imperfect field. If a ∈ k is not a p-th power, the polynomial X ^ p - a is irreducible, and at its place on k(x) the function x ^ p - a is a prime element. For example, a may be the variable of k = 𝔽_p(a) (TauCeti.ratFunc_pow_ne_X). Expansions and residues at places with inseparable residue field therefore cannot be set up over k in the way they are at places with separable residue field. A coefficient field that is only linear over the prime field still exists (TauCeti.Place.exists_completionResidueFieldSection), and through it 𝒪̂_P and F̂_P are still isomorphic to F_P[[T]] and F_P((T)) as rings (TauCeti.Place.completionIntegersEquivPowerSeriesOfSection, TauCeti.Place.completionEquivLaurentSeriesOfSection).

Main results

• TauCeti.Place.pow_ne_algebraMap_completion: c has no p-th root in F̂_P.
• TauCeti.Place.isEmpty_algHom_residueField_completion: there is no k-algebra map F_P → F̂_P.
• TauCeti.Place.not_isSeparable_residueField: F_P is not separable over k.
• TauCeti.Place.isEmpty_completionIntegers_algEquiv_powerSeries and TauCeti.Place.isEmpty_completion_algEquiv_laurentSeries: 𝒪̂_P is not k-isomorphic to F_P[[T]], and F̂_P is not k-isomorphic to F_P((T)).
• TauCeti.Place.isEmpty_completionIntegers_algEquiv_powerSeries_adicOfIrreducible_X_pow_sub_C: the example of the place of an irreducible X ^ p - a on k(x).

References

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

theorem TauCeti.Place.pow_ne_algebraMap_completion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {p : ℕ} [ExpChar k p] {z : F} {c : k} (hz : ¬↑p ∣ P.ord (z ^ p - (algebraMap k F) c)) (b : P.Completion) : b ^ p ≠ (algebraMap k P.Completion) c

No p-th root of c in the completion. If z ^ p - c has order at P not divisible by p, then the constant c is not a p-th power in F̂_P: otherwise z ^ p - c = (z - b) ^ p there.

theorem TauCeti.Place.isEmpty_algHom_residueField_completion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {p : ℕ} [ExpChar k p] {z : F} {c : k} (hpos : 0 < P.ord (z ^ p - (algebraMap k F) c)) (hz : ¬↑p ∣ P.ord (z ^ p - (algebraMap k F) c)) : IsEmpty (P.ResidueField →ₐ[k] P.Completion)

No k-algebra map from the residue field to the completion. If z ^ p - c has positive order at P, not divisible by p, then z(P) is a p-th root of c in F_P, which F̂_P does not have.

theorem TauCeti.Place.not_isSeparable_residueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {p : ℕ} [ExpChar k p] {z : F} {c : k} (hpos : 0 < P.ord (z ^ p - (algebraMap k F) c)) (hz : ¬↑p ∣ P.ord (z ^ p - (algebraMap k F) c)) : ¬Algebra.IsSeparable k P.ResidueField

The residue field is inseparable over k when some z ^ p - c has positive order at P, not divisible by p: otherwise TauCeti.Place.completionResidueFieldSection would be a k-algebra map from F_P to the completion.

theorem TauCeti.Place.isEmpty_completionIntegers_algEquiv_powerSeries {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {p : ℕ} [ExpChar k p] {z : F} {c : k} (hpos : 0 < P.ord (z ^ p - (algebraMap k F) c)) (hz : ¬↑p ∣ P.ord (z ^ p - (algebraMap k F) c)) : IsEmpty (↥P.completionPlace.integers ≃ₐ[k] PowerSeries P.ResidueField)

The completed valuation ring is not F_P[[T]] over k when some z ^ p - c has positive order at P, not divisible by p: the separability hypothesis of TauCeti.Place.completionIntegersEquivPowerSeriesResidueField cannot be dropped.

theorem TauCeti.Place.isEmpty_completion_algEquiv_laurentSeries {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {p : ℕ} [ExpChar k p] {z : F} {c : k} (hpos : 0 < P.ord (z ^ p - (algebraMap k F) c)) (hz : ¬↑p ∣ P.ord (z ^ p - (algebraMap k F) c)) : IsEmpty (P.Completion ≃ₐ[k] LaurentSeries P.ResidueField)

The completion is not F_P((T)) over k when some z ^ p - c has positive order at P, not divisible by p: the separability hypothesis of TauCeti.Place.completionEquivLaurentSeriesResidueField cannot be dropped.

The place of X ^ p - a over an imperfect field

theorem TauCeti.Place.isEmpty_completionIntegers_algEquiv_powerSeries_adicOfIrreducible_X_pow_sub_C {k : Type u_1} [Field k] {p : ℕ} [ExpChar k p] {a : k} (hq : Irreducible (Polynomial.X ^ p - Polynomial.C a)) (hp : p ≠ 1) : IsEmpty (↥(adicOfIrreducible hq).completionPlace.integers ≃ₐ[k] PowerSeries (adicOfIrreducible hq).ResidueField)

The completion of k(x) at the place of an irreducible X ^ p - a is not F_P[[T]] over k: the residue field k[X] / (X ^ p - a) has no copy over k in the completed valuation ring. For p prime, X ^ p - a is irreducible as soon as a is not a p-th power (irreducible_X_pow_sub_C_of_prime), so this happens over every imperfect field, for example over 𝔽_p(a) (TauCeti.ratFunc_pow_ne_X). The hypothesis p ≠ 1 excludes characteristic zero, where the place of X - a is rational.