Constants are integrally closed in Laurent series

For a field K, the Laurent series algebraic over K are the constants: K is integrally closed in K⸨X⸩. A Laurent series integral over K is integral over K⟦X⟧, so it is a power series, because K⟦X⟧ is integrally closed in its fraction field K⸨X⸩; and the power series integral over K are the constants (PowerSeries.isIntegrallyClosedIn).

For instance a root of unity of K⸨X⸩ is a constant root of unity. This is what identifies the automorphisms of a ramified extension K⸨X⸩ ⊆ K⸨u⸩, u ^ d = X, with rescalings u ↦ η u by roots of unity η ∈ K, for every field K.

Main results

• TauCeti.LaurentSeries.isIntegrallyClosedIn: K is integrally closed in K⸨X⸩.
• TauCeti.LaurentSeries.exists_rootsOfUnity_algebraMap_eq: a root of unity of K⸨X⸩ is the image of a root of unity of K.

instance TauCeti.LaurentSeries.isIntegrallyClosedIn (K : Type u_1) [Field K] : IsIntegrallyClosedIn K (LaurentSeries K)

A field K is integrally closed in K⸨X⸩: the Laurent series algebraic over K are the constants.

theorem TauCeti.LaurentSeries.exists_rootsOfUnity_algebraMap_eq {K : Type u_1} [Field K] {d : ℕ+} {w : LaurentSeries K} (hw : w ^ ↑d = 1) : ∃ (η : ↥(rootsOfUnity (↑d) K)), (algebraMap K (LaurentSeries K)) ↑↑η = w

A d-th root of unity of K⸨X⸩ is a constant: the image of a d-th root of unity of K. This holds because the constants are integrally closed in K⸨X⸩.