Documentation

TauCeti.RingTheory.LaurentSeries.Level.Adjoin

Ramified Laurent levels as radical extensions #

For a field K and a positive integer d, the parameter u of the ramified Laurent level K⸨u⸩ satisfies u ^ d = X, where X is the parameter of the base Laurent field K⸨X⸩. The power basis of the level shows that T ^ d - X is the minimal polynomial of u, hence is irreducible over K⸨X⸩. Thus both the wrapped level and its actual image inside the Puiseux field are obtained by adjoining this root.

These identifications provide the radical-extension presentation of finite Puiseux levels needed to apply Kummer and splitting-field results.

Main results #

source
@[simp]
theorem TauCeti.LaurentSeries.Level.minpoly_parameter (K : Type u_1) [Field K] (d : ℕ+) :
minpoly (LaurentSeries K) (parameter K d) = Polynomial.X ^ ↑d - Polynomial.C ((HahnSeries.single 1) 1)

The minimal polynomial of the level parameter u is T ^ d - X.

source
@[simp]
theorem TauCeti.LaurentSeries.Level.adjoin_parameter_eq_top (K : Type u_1) [Field K] (d : ℕ+) :
(LaurentSeries K)⟮parameter K d⟯ = ⊤

The wrapped ramified level is generated over the base Laurent field by its parameter.

source
theorem TauCeti.LaurentSeries.irreducible_X_pow_sub_C_single (K : Type u_1) [Field K] (d : ℕ+) :
Irreducible (Polynomial.X ^ ↑d - Polynomial.C ((HahnSeries.single 1) 1))

The radical polynomial T ^ d - X is irreducible over the Laurent-series field.

source
@[reducible, inline]
noncomputable abbrev TauCeti.puiseuxField.levelParameter (K : Type u_1) [Field K] (d : ℕ+) :
↥(level K d)

The distinguished parameter of the actual level-d subfield of the Puiseux field.

Instances For
    source
    theorem TauCeti.puiseuxField.levelParameter_pow (K : Type u_1) [Field K] (d : ℕ+) :
    levelParameter K d ^ ↑d = (algebraMap (LaurentSeries K) ↥(level K d)) ((HahnSeries.single 1) 1)

    The actual level parameter is a d-th root of the base Laurent parameter.

    source
    theorem TauCeti.puiseuxField.coe_levelParameter_pow (K : Type u_1) [Field K] (d : ℕ+) :
    ↑(levelParameter K d) ^ ↑d = (algebraMap (LaurentSeries K) ↥(puiseuxField K)) ((HahnSeries.single 1) 1)

    The level parameter t ^ (1 / d), viewed in the Puiseux field, is a d-th root of the base Laurent parameter.

    source
    theorem TauCeti.puiseuxField.minpoly_levelParameter (K : Type u_1) [Field K] (d : ℕ+) :
    minpoly (LaurentSeries K) (levelParameter K d) = Polynomial.X ^ ↑d - Polynomial.C ((HahnSeries.single 1) 1)

    The minimal polynomial of the actual level parameter is T ^ d - X.

    source
    theorem TauCeti.puiseuxField.adjoin_levelParameter_eq_top (K : Type u_1) [Field K] (d : ℕ+) :
    (LaurentSeries K)⟮levelParameter K d⟯ = ⊤

    Internally, the actual level is generated over the base Laurent field by its parameter.

    source
    theorem TauCeti.puiseuxField.level_eq_adjoin (K : Type u_1) [Field K] (d : ℕ+) :
    level K d = (LaurentSeries K)⟮↑(levelParameter K d)⟯

    As intermediate fields of the Puiseux field, level d is obtained by adjoining its distinguished parameter.