Laurent Series

Main Definitions

• Defines LaurentSeries as an abbreviation for HahnSeries ℤ.
• Defines hasseDeriv of a Laurent series with coefficients in a module over a ring.
• Provides a coercion PowerSeries R into LaurentSeries R given by HahnSeries.ofPowerSeries.
• Defines LaurentSeries.powerSeriesPart
• Defines the localization map LaurentSeries.of_powerSeries_localization which evaluates to HahnSeries.ofPowerSeries.
• Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying RatFunc.coeAlgHom.
• Study of the X-Adic valuation on the ring of Laurent series over a field

Main Results

• Basic properties of Hasse derivatives

About the X-Adic valuation:

• The (integral) valuation of a power series is the order of the first non-zero coefficient, see intValuation_le_iff_coeff_lt_eq_zero.
• The valuation of a Laurent series is the order of the first non-zero coefficient, see valuation_le_iff_coeff_lt_eq_zero.
• Every Laurent series of valuation less than (1 : ℤₘ₀) comes from a power series, see val_le_one_iff_eq_coe.

Implementation details

• Since LaurentSeries is just an abbreviation of HahnSeries ℤ _, the definition of the coefficients is given in terms of HahnSeries.coeff and this forces sometimes to go back-and-forth from X : LaurentSeries _ to single 1 1 : HahnSeries ℤ _.

@[reducible, inline]

abbrev LaurentSeries (R : Type u) [Zero R] : Type u

A LaurentSeries is implemented as a HahnSeries with value group ℤ.

Equations

• LaurentSeries R = HahnSeries ℤ R

@[simp]

theorem LaurentSeries.hasseDeriv_apply (R : Type u_2) {V : Type u_3} [AddCommGroup V] [Semiring R] [Module R V] (k : ℕ) (f : LaurentSeries V) : (LaurentSeries.hasseDeriv R k) f = HahnSeries.ofSuppBddBelow (fun (n : ℤ) => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯

def LaurentSeries.hasseDeriv (R : Type u_2) {V : Type u_3} [AddCommGroup V] [Semiring R] [Module R V] (k : ℕ) : LaurentSeries V →ₗ[R] LaurentSeries V

The Hasse derivative of Laurent series, as a linear map.

Equations

• One or more equations did not get rendered due to their size.

theorem LaurentSeries.hasseDeriv_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) (n : ℤ) : ((LaurentSeries.hasseDeriv R k) f).coeff n = Ring.choose (n + ↑k) k • f.coeff (n + ↑k)

instance LaurentSeries.instCoePowerSeries {R : Type u_1} [Semiring R] : Coe (PowerSeries R) (LaurentSeries R)

Equations

• LaurentSeries.instCoePowerSeries = { coe := ⇑(HahnSeries.ofPowerSeries ℤ R) }

@[simp]

theorem LaurentSeries.coeff_coe_powerSeries {R : Type u_1} [Semiring R] (x : PowerSeries R) (n : ℕ) : ((HahnSeries.ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff R n) x

def LaurentSeries.powerSeriesPart {R : Type u_1} [Semiring R] (x : LaurentSeries R) : PowerSeries R

This is a power series that can be multiplied by an integer power of X to give our Laurent series. If the Laurent series is nonzero, powerSeriesPart has a nonzero constant term.

Equations

• x.powerSeriesPart = PowerSeries.mk fun (n : ℕ) => x.coeff (HahnSeries.order x + ↑n)

@[simp]

theorem LaurentSeries.powerSeriesPart_coeff {R : Type u_1} [Semiring R] (x : LaurentSeries R) (n : ℕ) : (PowerSeries.coeff R n) x.powerSeriesPart = x.coeff (HahnSeries.order x + ↑n)

@[simp]

theorem LaurentSeries.powerSeriesPart_zero {R : Type u_1} [Semiring R] : LaurentSeries.powerSeriesPart 0 = 0

@[simp]

theorem LaurentSeries.powerSeriesPart_eq_zero {R : Type u_1} [Semiring R] (x : LaurentSeries R) : x.powerSeriesPart = 0 ↔ x = 0

@[simp]

theorem LaurentSeries.single_order_mul_powerSeriesPart {R : Type u_1} [Semiring R] (x : LaurentSeries R) : (HahnSeries.single (HahnSeries.order x)) 1 * (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = x

theorem LaurentSeries.ofPowerSeries_powerSeriesPart {R : Type u_1} [Semiring R] (x : LaurentSeries R) : (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = (HahnSeries.single (-HahnSeries.order x)) 1 * x

instance LaurentSeries.instAlgebraPowerSeries {R : Type u_1} [CommSemiring R] : Algebra (PowerSeries R) (LaurentSeries R)

Equations

• LaurentSeries.instAlgebraPowerSeries = (HahnSeries.ofPowerSeries ℤ R).toAlgebra

@[simp]

theorem LaurentSeries.coe_algebraMap {R : Type u_1} [CommSemiring R] : ⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = ⇑(HahnSeries.ofPowerSeries ℤ R)

instance LaurentSeries.of_powerSeries_localization {R : Type u_1} [CommRing R] : IsLocalization (Submonoid.powers PowerSeries.X) (LaurentSeries R)

The localization map from power series to Laurent series.

Equations

• ⋯ = ⋯

instance LaurentSeries.instIsFractionRingPowerSeries {K : Type u_2} [Field K] : IsFractionRing (PowerSeries K) (LaurentSeries K)

Equations

• ⋯ = ⋯

theorem PowerSeries.coe_zero {R : Type u_1} [Semiring R] : (HahnSeries.ofPowerSeries ℤ R) 0 = 0

theorem PowerSeries.coe_one {R : Type u_1} [Semiring R] : (HahnSeries.ofPowerSeries ℤ R) 1 = 1

theorem PowerSeries.coe_add {R : Type u_1} [Semiring R] (f : PowerSeries R) (g : PowerSeries R) : (HahnSeries.ofPowerSeries ℤ R) (f + g) = (HahnSeries.ofPowerSeries ℤ R) f + (HahnSeries.ofPowerSeries ℤ R) g

theorem PowerSeries.coe_sub {R' : Type u_2} [Ring R'] (f' : PowerSeries R') (g' : PowerSeries R') : (HahnSeries.ofPowerSeries ℤ R') (f' - g') = (HahnSeries.ofPowerSeries ℤ R') f' - (HahnSeries.ofPowerSeries ℤ R') g'

theorem PowerSeries.coe_neg {R' : Type u_2} [Ring R'] (f' : PowerSeries R') : (HahnSeries.ofPowerSeries ℤ R') (-f') = -(HahnSeries.ofPowerSeries ℤ R') f'

theorem PowerSeries.coe_mul {R : Type u_1} [Semiring R] (f : PowerSeries R) (g : PowerSeries R) : (HahnSeries.ofPowerSeries ℤ R) (f * g) = (HahnSeries.ofPowerSeries ℤ R) f * (HahnSeries.ofPowerSeries ℤ R) g

theorem PowerSeries.coeff_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) (i : ℤ) : ((HahnSeries.ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (PowerSeries.coeff R i.natAbs) f

theorem PowerSeries.coe_C {R : Type u_1} [Semiring R] (r : R) : (HahnSeries.ofPowerSeries ℤ R) ((PowerSeries.C R) r) = HahnSeries.C r

theorem PowerSeries.coe_X {R : Type u_1} [Semiring R] : (HahnSeries.ofPowerSeries ℤ R) PowerSeries.X = (HahnSeries.single 1) 1

@[simp]

theorem PowerSeries.coe_smul {R : Type u_1} [Semiring R] {S : Type u_3} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) : (HahnSeries.ofPowerSeries ℤ S) (r • x) = r • (HahnSeries.ofPowerSeries ℤ S) x

theorem PowerSeries.coe_pow {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) : (HahnSeries.ofPowerSeries ℤ R) (f ^ n) = (HahnSeries.ofPowerSeries ℤ R) f ^ n

def RatFunc.coeAlgHom (F : Type u) [Field F] : RatFunc F →ₐ[Polynomial F] LaurentSeries F

The coercion RatFunc F → LaurentSeries F as bundled alg hom.

Equations

• RatFunc.coeAlgHom F = RatFunc.liftAlgHom (Algebra.ofId (Polynomial F) (LaurentSeries F)) ⋯

def RatFunc.coeToLaurentSeries_fun {F : Type u} [Field F] : RatFunc F → LaurentSeries F

The coercion RatFunc F → LaurentSeries F as a function.

This is the implementation of coeToLaurentSeries.

Equations

• RatFunc.coeToLaurentSeries_fun = ⇑(RatFunc.coeAlgHom F)

instance RatFunc.coeToLaurentSeries {F : Type u} [Field F] : Coe (RatFunc F) (LaurentSeries F)

Equations

• RatFunc.coeToLaurentSeries = { coe := RatFunc.coeToLaurentSeries_fun }

theorem RatFunc.coe_def {F : Type u} [Field F] (f : RatFunc F) : ↑f = (RatFunc.coeAlgHom F) f

theorem RatFunc.coe_num_denom {F : Type u} [Field F] (f : RatFunc F) : ↑f = (HahnSeries.ofPowerSeries ℤ F) ↑f.num / (HahnSeries.ofPowerSeries ℤ F) ↑f.denom

theorem RatFunc.coe_injective {F : Type u} [Field F] : Function.Injective RatFunc.coeToLaurentSeries_fun

@[simp]

theorem RatFunc.coe_apply {F : Type u} [Field F] (f : RatFunc F) : (RatFunc.coeAlgHom F) f = ↑f

theorem RatFunc.coe_coe {F : Type u} [Field F] (P : Polynomial F) : (HahnSeries.ofPowerSeries ℤ F) ↑P = ↑↑P

@[simp]

theorem RatFunc.coe_zero {F : Type u} [Field F] : ↑0 = 0

theorem RatFunc.coe_ne_zero {F : Type u} [Field F] {f : Polynomial F} (hf : f ≠ 0) : ↑f ≠ 0

@[simp]

theorem RatFunc.coe_one {F : Type u} [Field F] : ↑1 = 1

@[simp]

theorem RatFunc.coe_add {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f + g) = ↑f + ↑g

@[simp]

theorem RatFunc.coe_sub {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f - g) = ↑f - ↑g

@[simp]

theorem RatFunc.coe_neg {F : Type u} [Field F] (f : RatFunc F) : ↑(-f) = -↑f

@[simp]

theorem RatFunc.coe_mul {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f * g) = ↑f * ↑g

@[simp]

theorem RatFunc.coe_pow {F : Type u} [Field F] (f : RatFunc F) (n : ℕ) : ↑(f ^ n) = ↑f ^ n

@[simp]

theorem RatFunc.coe_div {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f / g) = ↑f / ↑g

@[simp]

theorem RatFunc.coe_C {F : Type u} [Field F] (r : F) : ↑(RatFunc.C r) = HahnSeries.C r

@[simp]

theorem RatFunc.coe_smul {F : Type u} [Field F] (f : RatFunc F) (r : F) : ↑(r • f) = r • ↑f

@[simp]

theorem RatFunc.coe_X {F : Type u} [Field F] : ↑RatFunc.X = (HahnSeries.single 1) 1

theorem RatFunc.single_one_eq_pow {R : Type u_2} [Ring R] (n : ℕ) : (HahnSeries.single ↑n) 1 = (HahnSeries.single 1) 1 ^ n

theorem RatFunc.single_inv {F : Type u} [Field F] (d : ℤ) {α : F} (hα : α ≠ 0) : (HahnSeries.single (-d)) α⁻¹ = ((HahnSeries.single d) α)⁻¹

theorem RatFunc.single_zpow {F : Type u} [Field F] (n : ℤ) : (HahnSeries.single n) 1 = (HahnSeries.single 1) 1 ^ n

instance RatFunc.instAlgebraLaurentSeries {F : Type u} [Field F] : Algebra (RatFunc F) (LaurentSeries F)

Equations

• RatFunc.instAlgebraLaurentSeries = (RatFunc.coeAlgHom F).toAlgebra

theorem RatFunc.algebraMap_apply_div {F : Type u} [Field F] (p : Polynomial F) (q : Polynomial F) : (algebraMap (RatFunc F) (LaurentSeries F)) ((algebraMap (Polynomial F) (RatFunc F)) p / (algebraMap (Polynomial F) (RatFunc F)) q) = (algebraMap (Polynomial F) (LaurentSeries F)) p / (algebraMap (Polynomial F) (LaurentSeries F)) q

instance RatFunc.instIsScalarTowerPolynomialLaurentSeries {F : Type u} [Field F] : IsScalarTower (Polynomial F) (RatFunc F) (LaurentSeries F)

Equations

• ⋯ = ⋯

def PowerSeries.idealX (K : Type u_2) [Field K] : IsDedekindDomain.HeightOneSpectrum (PowerSeries K)

The prime ideal (X) of PowerSeries K, when K is a field, as a term of the HeightOneSpectrum.

Equations

• PowerSeries.idealX K = { asIdeal := Ideal.span {PowerSeries.X}, isPrime := ⋯, ne_bot := ⋯ }

theorem PowerSeries.intValuation_eq_of_coe {K : Type u_2} [Field K] (P : Polynomial K) : (Polynomial.idealX K).intValuation P = (PowerSeries.idealX K).intValuation ↑P

@[simp]

theorem PowerSeries.intValuation_X {K : Type u_2} [Field K] : (PowerSeries.idealX K).intValuationDef PowerSeries.X = ↑(Multiplicative.ofAdd (-1))

The integral valuation of the power series X : K⟦X⟧ equals (ofAdd -1) : ℤₘ₀

theorem RatFunc.valuation_eq_LaurentSeries_valuation (K : Type u_2) [Field K] (P : RatFunc K) : (Polynomial.idealX K).valuation P = (PowerSeries.idealX K).valuation ↑P

instance LaurentSeries.instValuedWithZeroMultiplicativeInt (K : Type u_2) [Field K] : Valued (LaurentSeries K) (WithZero (Multiplicative ℤ))

Equations

• LaurentSeries.instValuedWithZeroMultiplicativeInt K = Valued.mk' (PowerSeries.idealX K).valuation

theorem LaurentSeries.valuation_X_pow (K : Type u_2) [Field K] (s : ℕ) : Valued.v ((HahnSeries.ofPowerSeries ℤ K) PowerSeries.X ^ s) = ↑(Multiplicative.ofAdd (-↑s))

theorem LaurentSeries.valuation_single_zpow (K : Type u_2) [Field K] (s : ℤ) : Valued.v ((HahnSeries.single s) 1) = ↑(Multiplicative.ofAdd (-s))

theorem LaurentSeries.coeff_zero_of_lt_intValuation (K : Type u_2) [Field K] {n : ℕ} {d : ℕ} {f : PowerSeries K} (H : Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))) : n < d → (PowerSeries.coeff K n) f = 0

theorem LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {d : ℕ} (f : PowerSeries K) : Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0

theorem LaurentSeries.coeff_zero_of_lt_valuation (K : Type u_2) [Field K] {n : ℤ} {D : ℤ} {f : LaurentSeries K} (H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))) : n < D → f.coeff n = 0

theorem LaurentSeries.valuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {D : ℤ} {f : LaurentSeries K} : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D)) ↔ ∀ n < D, f.coeff n = 0

theorem LaurentSeries.eq_coeff_of_valuation_sub_lt (K : Type u_2) [Field K] {d : ℤ} {n : ℤ} {f : LaurentSeries K} {g : LaurentSeries K} (H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))) : n < d → g.coeff n = f.coeff n

theorem LaurentSeries.val_le_one_iff_eq_coe (K : Type u_2) [Field K] (f : LaurentSeries K) : Valued.v f ≤ 1 ↔ ∃ (F : PowerSeries K), (HahnSeries.ofPowerSeries ℤ K) F = f