The Kummer action on ramified Laurent levels

Let K be a field and d a positive integer. The ramified level K⸨u⸩, with u ^ d = X, is obtained from K⸨X⸩ by adjoining a root of T ^ d - X. Every d-th root of unity η of K gives a K⸨X⸩-algebra automorphism u ↦ η u of the level, the rescaling f (u) ↦ f (η u): it multiplies the coefficient of uᵏ by ηᵏ, so it fixes the series in u ^ d = X. Over every field K these are all the automorphisms of the level over K⸨X⸩: an automorphism σ sends u to another root of T ^ d - X, and σ u / u is a root of unity of K⸨X⸩, hence a constant.

When K has a primitive d-th root of unity, the level is a splitting field of T ^ d - X over K⸨X⸩, hence a Galois extension. Mathlib's Kummer theory (autEquivRootsOfUnity) identifies its Galois group with the d-th roots of unity, and the automorphism attached to η is exactly the rescaling above. So every Galois automorphism of the level is a coefficientwise rescaling.

The same statements are transported to the actual level-d subfield of the Puiseux field, the Laurent series in t ^ (1 / d). There the automorphism attached to η multiplies the coefficient of t ^ (k / d) by ηᵏ. For n ∣ m, the automorphism of level m attached to η restricts on level n to the automorphism attached to η ^ (m / n). These are the finite-level Galois actions out of which the absolute Galois group of K⸨X⸩ is assembled, when K is algebraically closed of characteristic zero.

Inside level m, the restriction formula identifies the fixed fields. The automorphism attached to η fixes level n exactly when η ^ (m / n) = 1. Conversely, if ω is a primitive (m / n)-th root of unity, a series of level m fixed by ω has its coefficient of t ^ (k / m) multiplied by ω ^ k, so it is supported on the exponents with m / n ∣ k, which are those of level n. Hence the fixed field of the group generated by ω is level n, and the automorphisms fixing level n are the powers of ω. When K has a primitive m-th root of unity, the Galois group of level m is cyclic, so every intermediate field of level m is the level of its degree.

Main definitions

• TauCeti.LaurentSeries.Level.kummer K d: the Kummer automorphisms u ↦ η u of the wrapped level K⸨u⸩, as a homomorphism from the d-th roots of unity of K to its Galois group.
• TauCeti.LaurentSeries.Level.galEquivRootsOfUnity K d: the Galois group of the level is the group of d-th roots of unity of K.
• TauCeti.puiseuxField.levelKummer K d and TauCeti.puiseuxField.levelGalEquivRootsOfUnity K d: the same for the actual level-d subfield of the Puiseux field.

Main results

• TauCeti.LaurentSeries.Level.kummer_parameter: the Kummer automorphism attached to η sends u to η u.
• TauCeti.LaurentSeries.Level.kummer_surjective: over every field, every automorphism of the level over K⸨X⸩ is a Kummer automorphism.
• TauCeti.LaurentSeries.Level.isSplittingField and TauCeti.LaurentSeries.Level.isGalois: with a primitive d-th root of unity in K, the level is a splitting field of T ^ d - X, hence Galois over K⸨X⸩.
• TauCeti.LaurentSeries.Level.galEquivRootsOfUnity_symm_apply: the Galois automorphism attached to η is the Kummer automorphism attached to η.
• TauCeti.puiseuxField.levelKummer_levelParameter: on the actual level, the Kummer automorphism attached to η sends t ^ (1 / d) to η t ^ (1 / d).
• TauCeti.puiseuxField.coeff_levelKummer: on the actual level, the Kummer automorphism attached to η multiplies the coefficient of t ^ (k / d) by ηᵏ.
• TauCeti.puiseuxField.levelKummer_inclusion: restriction of Kummer automorphisms from level m to level n, for n ∣ m, along the power map TauCeti.rootsOfUnityPowOfDvd.
• TauCeti.puiseuxField.levelKummer_injective: distinct roots of unity give distinct Kummer automorphisms.
• TauCeti.puiseuxField.levelKummer_mem_fixingSubgroup_restrict_iff: the Kummer automorphism of level m attached to η fixes level n exactly when η ^ (m / n) = 1.
• TauCeti.puiseuxField.levelKummer_apply_eq_self_iff and TauCeti.puiseuxField.fixedField_zpowers_levelKummer: for a primitive (m / n)-th root of unity ω, the series of level m fixed by ω are those of level n.
• TauCeti.puiseuxField.fixingSubgroup_restrict_eq_zpowers_levelKummer: the automorphisms of level m fixing level n are the powers of ω.
• TauCeti.puiseuxField.eq_restrict_level_of_finrank_eq: with a primitive d-th root of unity in K, an intermediate field of level d of degree e is level e.

noncomputable def TauCeti.LaurentSeries.Level.kummer (K : Type u_1) [Field K] (d : ℕ+) : ↥(rootsOfUnity (↑d) K) →* Gal(Level K d/LaurentSeries K)

The Kummer automorphisms u ↦ η u of the ramified level K⸨u⸩ over K⸨X⸩ = K⸨u ^ d⸩, attached to the d-th roots of unity η of the coefficient field. On underlying Laurent series the automorphism attached to η is the rescaling f (u) ↦ f (η u).

@[simp]

theorem TauCeti.LaurentSeries.Level.ringEquivLaurentSeries_kummer {K : Type u_1} [Field K] {d : ℕ+} (η : ↥(rootsOfUnity (↑d) K)) (f : Level K d) : (ringEquivLaurentSeries K d) (((kummer K d) η) f) = (rescale ↑η) ((ringEquivLaurentSeries K d) f)

On underlying Laurent series, the Kummer automorphism attached to η is rescaling by η.

@[simp]

theorem TauCeti.LaurentSeries.Level.kummer_parameter {K : Type u_1} [Field K] {d : ℕ+} (η : ↥(rootsOfUnity (↑d) K)) : ((kummer K d) η) (parameter K d) = (Algebra.algebraMap (LaurentSeries K) (Level K d)) ((Algebra.algebraMap K (LaurentSeries K)) ↑↑η) * parameter K d

The Kummer automorphism attached to η multiplies the level parameter by η.

theorem TauCeti.LaurentSeries.Level.kummer_surjective {K : Type u_1} [Field K] {d : ℕ+} : Function.Surjective ⇑(kummer K d)

Over every field K, every automorphism σ of the ramified level K⸨u⸩ over K⸨X⸩ is a Kummer automorphism u ↦ η u. Indeed σ u / u is a d-th root of unity of K⸨X⸩, and the constants are integrally closed in K⸨X⸩, so it is a root of unity η of K.

theorem TauCeti.LaurentSeries.Level.coeff_zero_apply_eq_of_algEquiv {K : Type u_1} [Field K] {d : ℕ+} {L : Type u_2} [Semiring L] [Algebra (LaurentSeries K) L] (φ ψ : L ≃ₐ[LaurentSeries K] Level K d) (x : L) : ((ringEquivLaurentSeries K d) (φ x)).coeff 0 = ((ringEquivLaurentSeries K d) (ψ x)).coeff 0

The constant coefficient of a level expansion is independent of the level isomorphism.

instance TauCeti.LaurentSeries.Level.isSplittingField (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] : Polynomial.IsSplittingField (LaurentSeries K) (Level K d) (Polynomial.X ^ ↑d - Polynomial.C ((HahnSeries.single 1) 1))

If the coefficient field has a primitive d-th root of unity, then the ramified level K⸨u⸩ is a splitting field of T ^ d - X over K⸨X⸩: its roots are the η u.

instance TauCeti.LaurentSeries.Level.isGalois (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] : IsGalois (LaurentSeries K) (Level K d)

If the coefficient field has a primitive d-th root of unity, then the ramified level K⸨u⸩ is a Galois extension of K⸨X⸩.

noncomputable def TauCeti.LaurentSeries.Level.galEquivRootsOfUnity (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] : Gal(Level K d/LaurentSeries K) ≃* ↥(rootsOfUnity (↑d) K)

If the coefficient field has a primitive d-th root of unity, then the Galois group of the ramified level K⸨u⸩ over K⸨X⸩ is the group of d-th roots of unity of K. An automorphism σ corresponds to the root of unity σ u / u, and the inverse is kummer (TauCeti.LaurentSeries.Level.galEquivRootsOfUnity_symm_apply).

@[simp]

theorem TauCeti.LaurentSeries.Level.galEquivRootsOfUnity_symm_apply (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] (η : ↥(rootsOfUnity (↑d) K)) : (galEquivRootsOfUnity K d).symm η = (kummer K d) η

The Galois automorphism attached to a root of unity η is the Kummer automorphism u ↦ η u.

@[simp]

theorem TauCeti.LaurentSeries.Level.galEquivRootsOfUnity_kummer (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] (η : ↥(rootsOfUnity (↑d) K)) : (galEquivRootsOfUnity K d) ((kummer K d) η) = η

The root of unity attached to the Kummer automorphism u ↦ η u is η.

noncomputable def TauCeti.puiseuxField.levelKummer (K : Type u_1) [Field K] (d : ℕ+) : ↥(rootsOfUnity (↑d) K) →* Gal(↥(level K d)/LaurentSeries K)

The Kummer automorphisms t ^ (1 / d) ↦ η t ^ (1 / d) of the actual level-d subfield of the Puiseux field, attached to the d-th roots of unity η of the coefficient field. The automorphism attached to η multiplies the coefficient of t ^ (k / d) by ηᵏ (TauCeti.puiseuxField.coeff_levelKummer).

@[simp]

theorem TauCeti.puiseuxField.levelKummer_levelEquiv {K : Type u_1} [Field K] {d : ℕ+} (η : ↥(rootsOfUnity (↑d) K)) (f : LaurentSeries.Level K d) : ((levelKummer K d) η) ((levelEquiv K d) f) = (levelEquiv K d) (((LaurentSeries.Level.kummer K d) η) f)

The Kummer automorphisms of the actual level correspond to those of the wrapped level under levelEquiv.

theorem TauCeti.puiseuxField.levelKummer_levelParameter {K : Type u_1} [Field K] {d : ℕ+} (η : ↥(rootsOfUnity (↑d) K)) : ((levelKummer K d) η) (levelParameter K d) = (algebraMap (LaurentSeries K) ↥(level K d)) ((algebraMap K (LaurentSeries K)) ↑↑η) * levelParameter K d

The Kummer automorphism attached to η multiplies the actual level parameter t ^ (1 / d) by η. This is not a simp lemma: simp already computes it through levelPowerBasis_gen, levelKummer_levelEquiv and TauCeti.LaurentSeries.Level.kummer_parameter.

theorem TauCeti.puiseuxField.coe_levelKummer_of_coe_eq {K : Type u_1} [Field K] {d : ℕ+} (η : ↥(rootsOfUnity (↑d) K)) {x : ↥(level K d)} {f : LaurentSeries K} (hx : ↑x = (levelEmbedding K d) f) : ↑(((levelKummer K d) η) x) = (levelEmbedding K d) ((LaurentSeries.rescale ↑η) f)

If x is the level-d image of the Laurent series f, then its image under the Kummer automorphism attached to η is the level-d image of the rescaled series f (η X).

@[simp]

theorem TauCeti.puiseuxField.coeff_levelKummer {K : Type u_1} [Field K] {d : ℕ+} (η : ↥(rootsOfUnity (↑d) K)) (x : ↥(level K d)) (k : ℤ) : (↑↑(((levelKummer K d) η) x)).coeff (↑k / ↑↑d) = ↑↑η ^ k * (↑↑x).coeff (↑k / ↑↑d)

The Kummer automorphism attached to η multiplies the coefficient of t ^ (k / d) by ηᵏ. The other coefficients of a level-d series vanish (LaurentSeries.coeff_ramifiedEmbedding_of_not_den_dvd).

theorem TauCeti.puiseuxField.levelKummer_injective {K : Type u_1} [Field K] {d : ℕ+} : Function.Injective ⇑(levelKummer K d)

Faithfulness. Distinct roots of unity give distinct Kummer automorphisms of level d: the automorphism attached to η multiplies t ^ (1 / d) by η.

theorem TauCeti.puiseuxField.levelKummer_inclusion {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) (η : ↥(rootsOfUnity (↑m) K)) (x : ↥(level K n)) : ((levelKummer K m) η) ((IntermediateField.inclusion ⋯) x) = (IntermediateField.inclusion ⋯) (((levelKummer K n) ((rootsOfUnityPowOfDvd ⋯) η)) x)

Restriction of Kummer automorphisms. For n ∣ m, the Kummer automorphism of level m attached to η restricts on level n to the Kummer automorphism attached to η ^ (m / n).

theorem TauCeti.puiseuxField.levelKummer_mem_fixingSubgroup_restrict_iff {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) (η : ↥(rootsOfUnity (↑m) K)) : (levelKummer K m) η ∈ (IntermediateField.restrict ⋯).fixingSubgroup ↔ ↑η ^ (↑m / ↑n) = 1

For n ∣ m, the Kummer automorphism of level m attached to η fixes level n exactly when η ^ (m / n) = 1, since it acts on level n through η ^ (m / n). This holds over every field K.

theorem TauCeti.puiseuxField.levelKummer_apply_eq_self_iff {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) {ω : ↥(rootsOfUnity (↑m) K)} (hω : IsPrimitiveRoot (↑ω) (↑m / ↑n)) (x : ↥(level K m)) : ((levelKummer K m) ω) x = x ↔ ↑x ∈ level K n

Fixed fields. For n ∣ m, let ω be an m-th root of unity of K that is a primitive (m / n)-th root of unity. A series of level m is fixed by the Kummer automorphism attached to ω exactly when it lies in level n.

theorem TauCeti.puiseuxField.fixedField_zpowers_levelKummer {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) {ω : ↥(rootsOfUnity (↑m) K)} (hω : IsPrimitiveRoot (↑ω) (↑m / ↑n)) : IntermediateField.fixedField (Subgroup.zpowers ((levelKummer K m) ω)) = IntermediateField.restrict ⋯

Fixed fields. For n ∣ m, let ω be an m-th root of unity of K that is a primitive (m / n)-th root of unity. The fixed field in level m of the group generated by the Kummer automorphism attached to ω is level n.

theorem TauCeti.puiseuxField.fixingSubgroup_restrict_eq_zpowers_levelKummer {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) {ω : ↥(rootsOfUnity (↑m) K)} (hω : IsPrimitiveRoot (↑ω) (↑m / ↑n)) : (IntermediateField.restrict ⋯).fixingSubgroup = Subgroup.zpowers ((levelKummer K m) ω)

Stabilizers. For n ∣ m, let ω be an m-th root of unity of K that is a primitive (m / n)-th root of unity. The automorphisms of level m over K⸨X⸩ fixing level n are the powers of the Kummer automorphism attached to ω.

instance TauCeti.puiseuxField.isGalois_level (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] : IsGalois (LaurentSeries K) ↥(level K d)

If the coefficient field has a primitive d-th root of unity, then the level-d subfield of the Puiseux field is a Galois extension of K⸨X⸩.

instance TauCeti.puiseuxField.normal_level (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] : Normal (LaurentSeries K) ↥(level K d)

If the coefficient field has a primitive d-th root of unity, then the level-d subfield of the Puiseux field is a normal extension of K⸨X⸩, so Galois automorphisms of larger fields restrict to it. Instance search does not find this through isGalois_level in reasonable time.

noncomputable def TauCeti.puiseuxField.levelGalEquivRootsOfUnity (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] : Gal(↥(level K d)/LaurentSeries K) ≃* ↥(rootsOfUnity (↑d) K)

If the coefficient field has a primitive d-th root of unity, then the Galois group of the level-d subfield of the Puiseux field over K⸨X⸩ is the group of d-th roots of unity of K. The inverse is levelKummer (TauCeti.puiseuxField.levelGalEquivRootsOfUnity_symm_apply).

@[simp]

theorem TauCeti.puiseuxField.levelGalEquivRootsOfUnity_symm_apply (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] (η : ↥(rootsOfUnity (↑d) K)) : (levelGalEquivRootsOfUnity K d).symm η = (levelKummer K d) η

The Galois automorphism of the level-d subfield attached to a root of unity η is the Kummer automorphism t ^ (1 / d) ↦ η t ^ (1 / d).

@[simp]

theorem TauCeti.puiseuxField.levelGalEquivRootsOfUnity_levelKummer (K : Type u_1) [Field K] (d : ℕ+) [HasEnoughRootsOfUnity K ↑d] (η : ↥(rootsOfUnity (↑d) K)) : (levelGalEquivRootsOfUnity K d) ((levelKummer K d) η) = η

The root of unity attached to the Kummer automorphism attached to η is η.

theorem TauCeti.puiseuxField.eq_restrict_level_of_finrank_eq {K : Type u_1} [Field K] {d : ℕ+} [HasEnoughRootsOfUnity K ↑d] {e : ℕ+} {E : IntermediateField (LaurentSeries K) ↥(level K d)} (he : e ∣ d) (h : Module.finrank (LaurentSeries K) ↥E = ↑e) : E = IntermediateField.restrict ⋯

Intermediate fields of a level. If K has a primitive d-th root of unity, then an intermediate field of level d of degree e over K⸨X⸩ is level e: the Galois group of level d is cyclic, so it has a single intermediate field of each degree.