The Kummer action of compatible roots of unity on Puiseux series

A point ζ = (ζₙ)ₙ of the Tate module lim_n μₙ(K) of the roots of unity of K, the compatible families ζₘ ^ (m / n) = ζₙ for n ∣ m, acts on the Puiseux field by the K⸨X⸩-algebra automorphism t ^ (k / n) ↦ ζₙ ^ k t ^ (k / n). Concretely the automorphism multiplies the coefficient of t ^ q by ζ_{q.den} ^ q.num: it is the twist of rational Hahn series by the character TauCeti.PrimeToPTateModule.ratChar, which preserves supports and is trivial on integer exponents.

On the level-n subfield K⸨t ^ (1 / n)⸩ this automorphism restricts to the Kummer automorphism t ^ (1 / n) ↦ ζₙ t ^ (1 / n), so the action assembles the finite-level Kummer actions of TauCeti.puiseuxField.levelKummer compatibly with the transition maps. The action is faithful. If every ζₙ is a primitive n-th root of unity, the series fixed by ζ ^ n are exactly those of level n; in particular the series fixed by ζ are the Laurent series in t. When K is algebraically closed of characteristic zero, these automorphisms are the candidates for the whole absolute Galois group of K⸨X⸩ acting on the Puiseux field; that identification is not proved here.

The Tate module lim_n μₙ(K) is TauCeti.PrimeToPTateModule 1 K: every positive integer is prime to 1, so it is the inverse limit of all the finite groups μₙ(K) along the power maps, with the inverse-limit topology of these discrete groups.

Main definitions

• TauCeti.puiseuxField.kummer K: the action of lim_n μₙ(K) on the Puiseux field by K⸨X⸩-algebra automorphisms, t ^ (k / n) ↦ ζₙ ^ k t ^ (k / n).

Main results

• TauCeti.puiseuxField.coeff_kummer: the automorphism attached to ζ multiplies the coefficient of t ^ q by the value of the character of ζ at q.
• TauCeti.puiseuxField.coeff_kummer_intCast_div: it multiplies the coefficient of t ^ (k / n) by ζₙ ^ k.
• TauCeti.puiseuxField.kummer_coe_level: on the level-n subfield it is the Kummer automorphism TauCeti.puiseuxField.levelKummer attached to ζₙ.
• TauCeti.puiseuxField.kummer_injective: the action is faithful.
• TauCeti.puiseuxField.fixedField_zpowers_kummer_pow: if every ζₙ is primitive, the fixed field of ζ ^ n is the level-n subfield.
• TauCeti.puiseuxField.fixedField_zpowers_kummer: if every ζₙ is primitive, the fixed field of ζ is K⸨X⸩.

noncomputable def TauCeti.puiseuxField.kummer (K : Type u_1) [Field K] : PrimeToPTateModule 1 K →* Gal(↥(puiseuxField K)/LaurentSeries K)

The Kummer action of the Tate module lim_n μₙ(K) on the Puiseux field: the point ζ = (ζₙ)ₙ acts by the K⸨X⸩-algebra automorphism t ^ (k / n) ↦ ζₙ ^ k t ^ (k / n), which multiplies the coefficient of t ^ q by ζ_{q.den} ^ q.num.

theorem TauCeti.puiseuxField.coe_kummer_apply {K : Type u_1} [Field K] (ζ : PrimeToPTateModule 1 K) (x : ↥(puiseuxField K)) : ↑(((kummer K) ζ) x) = (HahnSeries.twistEquiv ((PrimeToPTateModule.ratChar K) ζ)) ↑x

As a Hahn series, the image of x under the automorphism attached to ζ is the twist of x by the character of ζ.

@[simp]

theorem TauCeti.puiseuxField.coeff_kummer {K : Type u_1} [Field K] (ζ : PrimeToPTateModule 1 K) (x : ↥(puiseuxField K)) (q : ℚ) : (↑(((kummer K) ζ) x)).coeff q = ↑(((PrimeToPTateModule.ratChar K) ζ) (Multiplicative.ofAdd q)) * (↑x).coeff q

The automorphism attached to ζ multiplies the coefficient of t ^ q by the value of the character of ζ at q, that is, by ζ_{q.den} ^ q.num.

theorem TauCeti.puiseuxField.coeff_kummer_intCast_div {K : Type u_1} [Field K] (ζ : PrimeToPTateModule 1 K) (x : ↥(puiseuxField K)) (n : ℕ+) (k : ℤ) : (↑(((kummer K) ζ) x)).coeff (↑k / ↑↑n) = ↑↑((PrimeToPTateModule.proj ⟨↑n, ⋯⟩) ζ) ^ k * (↑x).coeff (↑k / ↑↑n)

The automorphism attached to ζ multiplies the coefficient of t ^ (k / n) by ζₙ ^ k.

@[simp]

theorem TauCeti.puiseuxField.kummer_single {K : Type u_1} [Field K] (ζ : PrimeToPTateModule 1 K) (q : ℚ) (a : K) : ((kummer K) ζ) (single K q a) = single K q (↑(((PrimeToPTateModule.ratChar K) ζ) (Multiplicative.ofAdd q)) * a)

The automorphism attached to ζ sends the monomial a t ^ q to ζ_{q.den} ^ q.num a t ^ q, where ζ_{q.den} ^ q.num is the value of the character of ζ at q.

theorem TauCeti.puiseuxField.kummer_coe_level {K : Type u_1} [Field K] (ζ : PrimeToPTateModule 1 K) {n : ℕ+} (x : ↥(level K n)) : ((kummer K) ζ) ↑x = ↑(((levelKummer K n) ((PrimeToPTateModule.proj ⟨↑n, ⋯⟩) ζ)) x)

Compatibility with the finite levels. On the level-n subfield K⸨t ^ (1 / n)⸩, the automorphism attached to ζ is the Kummer automorphism t ^ (1 / n) ↦ ζₙ t ^ (1 / n).

theorem TauCeti.puiseuxField.kummer_injective {K : Type u_1} [Field K] : Function.Injective ⇑(kummer K)

Faithfulness. Distinct points of the Tate module act by distinct automorphisms of the Puiseux field: the automorphism attached to ζ sends t ^ (1 / n) to ζₙ t ^ (1 / n).

theorem TauCeti.puiseuxField.fixedField_zpowers_kummer_pow {K : Type u_1} [Field K] {ζ : PrimeToPTateModule 1 K} (hζ : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime 1 }), IsPrimitiveRoot ↑((PrimeToPTateModule.proj m) ζ) ↑m) (n : ℕ+) : IntermediateField.fixedField (Subgroup.zpowers ((kummer K) ζ ^ ↑n)) = level K n

Fixed fields. If every component ζₙ of ζ is a primitive n-th root of unity, then the Puiseux series fixed by ζ ^ n are exactly those of level n.

theorem TauCeti.puiseuxField.fixedField_zpowers_kummer {K : Type u_1} [Field K] {ζ : PrimeToPTateModule 1 K} (hζ : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime 1 }), IsPrimitiveRoot ↑((PrimeToPTateModule.proj m) ζ) ↑m) : IntermediateField.fixedField (Subgroup.zpowers ((kummer K) ζ)) = ⊥

If every component ζₙ of ζ is a primitive n-th root of unity, then the Puiseux series fixed by ζ are exactly the Laurent series in t.