Laurent series over a finite field form a local field

For a field K, the formal Laurent series K⸨X⸩ carry Mathlib's X-adic valuation LaurentSeries.valued. This file equips K⸨X⸩ with the valuative relation that valuation induces, checks that the X-adic topology is the valuative topology and that the relation is nontrivial, and identifies the ring of integers of the relation with the power series and its residue field with K. When K is finite, K⸨X⸩ is a nonarchimedean local field: it is the equal-characteristic local field 𝔽_q((X)), with residue field 𝔽_q.

Main results

• TauCeti.LaurentSeries.integer_eq_powerSeries_as_subring: the ring of integers 𝒪[K⸨X⸩] is the subring of power series.
• TauCeti.LaurentSeries.valuativeResidueFieldEquiv: the residue field 𝓀[K⸨X⸩] is K, the residue of an integer being its constant coefficient (TauCeti.LaurentSeries.valuativeResidueFieldEquiv_residue); hence TauCeti.LaurentSeries.natCard_residueField and TauCeti.LaurentSeries.ringChar_residueField.
• TauCeti.LaurentSeries.isNonarchimedeanLocalField: for a finite field K, K⸨X⸩ is a nonarchimedean local field.

Implementation notes

Local compactness is transported from the X-adic completion of K⟮X⟯, which is a nonarchimedean local field by IsDedekindDomain.HeightOneSpectrum.isNonarchimedeanLocalField_adicCompletion, along Mathlib's uniform equivalence LaurentSeries.comparePkg between that completion and K⸨X⸩.

References

• J.-P. Serre, Local Fields, Chapter II, where the complete discretely valued fields of equal characteristic with perfect residue field k are identified with k((X)).

@[instance_reducible]

noncomputable instance TauCeti.LaurentSeries.instValuativeRel (K : Type u_1) [Field K] : ValuativeRel (LaurentSeries K)

The valuative relation on K⸨X⸩ induced by its X-adic valuation.

instance TauCeti.LaurentSeries.instCompatibleValued (K : Type u_1) [Field K] : Valued.v.Compatible

The X-adic valuation is compatible with the valuative relation it induces.

instance TauCeti.LaurentSeries.isValuativeTopology (K : Type u_1) [Field K] : IsValuativeTopology (LaurentSeries K)

The X-adic topology of K⸨X⸩ is induced by its valuative relation.

instance TauCeti.LaurentSeries.isNontrivial (K : Type u_1) [Field K] : ValuativeRel.IsNontrivial (LaurentSeries K)

The valuative relation on K⸨X⸩ is nontrivial: X has valuation exp (-1).

theorem TauCeti.LaurentSeries.integer_eq_powerSeries_as_subring (K : Type u_1) [Field K] : (ValuativeRel.valuation (LaurentSeries K)).integer = LaurentSeries.powerSeries_as_subring K

The ring of integers of the valuative relation on K⸨X⸩ is the subring of power series.

noncomputable def TauCeti.LaurentSeries.valuativeResidueFieldEquiv (K : Type u_1) [Field K] : IsLocalRing.ResidueField ↥(ValuativeRel.valuation (LaurentSeries K)).integer ≃+* K

The residue field of the valuative relation on K⸨X⸩ is the coefficient field K.

@[simp]

theorem TauCeti.LaurentSeries.valuativeResidueFieldEquiv_residue (K : Type u_1) [Field K] (f : ↥(ValuativeRel.valuation (LaurentSeries K)).integer) : (valuativeResidueFieldEquiv K) ((IsLocalRing.residue ↥(ValuativeRel.valuation (LaurentSeries K)).integer) f) = (↑f).coeff 0

The residue of an integer of K⸨X⸩ is its constant coefficient.

@[simp]

theorem TauCeti.LaurentSeries.natCard_residueField (K : Type u_1) [Field K] : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (LaurentSeries K)).integer) = Nat.card K

The residue field of K⸨X⸩ has as many elements as K.

@[simp]

theorem TauCeti.LaurentSeries.ringChar_residueField (K : Type u_1) [Field K] : ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (LaurentSeries K)).integer) = ringChar K

The residue characteristic of K⸨X⸩ is the characteristic of K.

instance TauCeti.LaurentSeries.isNonarchimedeanLocalField (K : Type u_1) [Field K] [Finite K] : IsNonarchimedeanLocalField (LaurentSeries K)

𝔽_q((X)) is a nonarchimedean local field. For a finite field K, the Laurent series K⸨X⸩, with their X-adic topology and valuation, form a nonarchimedean local field.