Documentation

TauCeti.RingTheory.LaurentSeries.Puiseux.FiniteExtension

Finite extensions of the Laurent-series field #

Let K be a field containing a primitive n-th root of unity for every n > 0 (so of characteristic zero). This file proves that the finite extensions of K⸨X⸩ inside the Puiseux field are exactly the ramified levels K⸨t ^ (1 / e)⸩, one for each degree e. When K is moreover algebraically closed, every finite extension of K⸨X⸩ of degree e is therefore isomorphic over K⸨X⸩ to the level K⸨u⸩ with u ^ e = X.

A finite-dimensional intermediate field E of the Puiseux field is spanned by finitely many Puiseux series, so it lies in a single level n. The level n is a Galois extension of K⸨X⸩ with cyclic Galois group μₙ(K). A cyclic group has at most one subgroup of each index, so by the Galois correspondence E is the unique intermediate field of level n of degree [E : K⸨X⸩], namely the level of that degree.

Consequently a Puiseux series x generates the level [K⸨X⸩(x) : K⸨X⸩], it lies in level n exactly when this degree divides n, and a root of a nonzero polynomial of degree d over K⸨X⸩ lies in level d!. The trace formula for the levels then holds for every finite extension E inside the Puiseux field: the trace from E multiplies the integer-exponent coefficients by [E : K⸨X⸩].

Main results #

source
theorem TauCeti.puiseuxField.eq_level_of_finrank_eq {K : Type u_1} [Field K] [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] {E : IntermediateField (LaurentSeries K) ↥(puiseuxField K)} {e : ℕ+} (h : Module.finrank (LaurentSeries K) ↥E = ↑e) :
E = level K e

If K contains all roots of unity, then an intermediate field of the Puiseux field of degree e over K⸨X⸩ is the level-e subfield K⸨t ^ (1 / e)⸩.

source
theorem TauCeti.puiseuxField.adjoin_simple_eq_level {K : Type u_1} [Field K] [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] (x : ↥(puiseuxField K)) :
(LaurentSeries K)⟮x⟯ = level K (Module.finrank (LaurentSeries K) ↥(LaurentSeries K)⟮x⟯).toPNat'

If K contains all roots of unity, then the intermediate field generated by a Puiseux series x is the level of degree [K⸨X⸩(x) : K⸨X⸩].

source
theorem TauCeti.puiseuxField.mem_level_iff_finrank_adjoin_dvd {K : Type u_1} [Field K] [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] {x : ↥(puiseuxField K)} {n : ℕ+} :
x ∈ level K n ↔ Module.finrank (LaurentSeries K) ↥(LaurentSeries K)⟮x⟯ ∣ ↑n

If K contains all roots of unity, then a Puiseux series x lies in level n exactly when the degree [K⸨X⸩(x) : K⸨X⸩] divides n. In particular this degree is the least level containing x.

source
theorem TauCeti.puiseuxField.mem_level_factorial_of_aeval_eq_zero {K : Type u_1} [Field K] [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] {p : Polynomial (LaurentSeries K)} (hp : p ≠ 0) {x : ↥(puiseuxField K)} (hx : (Polynomial.aeval x) p = 0) :
x ∈ level K p.natDegree.factorial.toPNat'

If K contains all roots of unity, then a Puiseux series that is a root of a nonzero polynomial of degree d over K⸨X⸩ lies in level d!. Thus all roots of such a polynomial lie in a common level.

source
noncomputable def TauCeti.LaurentSeries.Level.algEquivOfFinrankEq {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {L : Type u_2} [Field L] [Algebra (LaurentSeries K) L] {e : ℕ+} (h : Module.finrank (LaurentSeries K) L = ↑e) :
L ≃ₐ[LaurentSeries K] Level K e

Finite extensions of K⸨X⸩. If K is algebraically closed of characteristic zero, then every extension L of K⸨X⸩ of degree e is isomorphic over K⸨X⸩ to the ramified level K⸨u⸩, u ^ e = X. The isomorphism is a chosen one: it is built from a chosen embedding of L into the Puiseux field, whose image is the level-e subfield.

Instances For
    source
    theorem TauCeti.LaurentSeries.Level.nonempty_algEquiv_iff {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {L : Type u_2} [Field L] [Algebra (LaurentSeries K) L] {e : ℕ+} :
    Nonempty (L ≃ₐ[LaurentSeries K] Level K e) ↔ Module.finrank (LaurentSeries K) L = ↑e

    If K is algebraically closed of characteristic zero, then an extension of K⸨X⸩ is isomorphic over K⸨X⸩ to the ramified level K⸨u⸩, u ^ e = X, exactly when it has degree e.

    source
    theorem IntermediateField.finiteDimensional_iff_exists_eq_level {K : Type u_1} [Field K] [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] (E : IntermediateField (LaurentSeries K) ↥(TauCeti.puiseuxField K)) :
    FiniteDimensional (LaurentSeries K) ↥E ↔ ∃ (n : ℕ+), E = TauCeti.puiseuxField.level K n

    If K contains all roots of unity, then the finite-dimensional intermediate fields of the Puiseux field over K⸨X⸩ are exactly the ramified levels.

    source
    theorem TauCeti.puiseuxField.coeff_trace_of_finiteDimensional {K : Type u_1} [Field K] [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] {E : IntermediateField (LaurentSeries K) ↥(puiseuxField K)} [FiniteDimensional (LaurentSeries K) ↥E] (x : ↥E) (j : ℤ) :
    ((Algebra.trace (LaurentSeries K) ↥E) x).coeff j = Module.finrank (LaurentSeries K) ↥E • (↑↑x).coeff ↑j

    The trace of a finite extension inside the Puiseux field. If K contains all roots of unity and E is a finite extension of K⸨X⸩ inside the Puiseux field, then the coefficient of t ^ j in the trace of x ∈ E down to K⸨X⸩ is [E : K⸨X⸩] times the coefficient of t ^ j in x. For j = -1 this is Res_t (Tr_{E/K⸨X⸩} (x) dt) = [E : K⸨X⸩] • Res_t (x dt), with the residue on the right taken among rational exponents.