Laurent polynomials as Laurent series

Over any semiring, a Laurent polynomial is a Laurent series with finitely many nonzero coefficients. This file defines the ring homomorphism LaurentPolynomial.toLaurentSeries : R[T;T⁻¹] →+* R⸨X⸩ sending T to X, and shows that it preserves coefficients, so in particular it is injective. When R is commutative, this map gives R⸨X⸩ its canonical R[T;T⁻¹]-algebra structure. The resulting algebra towers make the two routes from polynomials to Laurent series agree: through power series and through Laurent polynomials. The image of the Laurent-polynomial map is exactly the Laurent series of finite support, and the order of a nonzero image is the least exponent in the Laurent polynomial's support.

For a Laurent series f, LaurentSeries.trunc N f retains the terms of exponent strictly less than N. These Laurent polynomials converge to f as N tends to infinity. Consequently, Laurent polynomials are dense in the Laurent-series field for its valuation topology.

The inclusion commutes with the formal derivatives LaurentPolynomial.derivative and LaurentSeries.derivative, so the derivative of Laurent series restricts to that of Laurent polynomials.

Main definitions

• LaurentPolynomial.toLaurentSeries: the inclusion of Laurent polynomials into Laurent series.
• LaurentSeries.algebraLaurentPolynomial: the induced Laurent-polynomial algebra structure.

Main results

• LaurentPolynomial.toLaurentSeries_T: Tⁿ is sent to Xⁿ, for every integer n.
• LaurentPolynomial.coeff_toLaurentSeries: the inclusion preserves coefficients.
• LaurentPolynomial.toLaurentSeries_injective: the inclusion is injective.
• LaurentPolynomial.toLaurentSeries_toLaurent: the polynomial embedding commutes with the inclusions into Laurent polynomials and power series.
• LaurentPolynomial.mem_range_toLaurentSeries_iff: the image consists exactly of the finite-support Laurent series.
• LaurentPolynomial.toLaurentSeries_derivative: the inclusion commutes with differentiation.
• LaurentSeries.finite_support_truncLT: strict truncation of a Laurent series has finite support.
• LaurentSeries.trunc: truncation of a Laurent series above a given integer exponent.
• LaurentSeries.trunc_eq_sum_Ico: the finite monomial expansion of a truncation.
• LaurentSeries.tendsto_toLaurentSeries_trunc: the truncations converge to the original series.
• LaurentPolynomial.denseRange_toLaurentSeries: Laurent polynomials are dense in Laurent series.
• LaurentSeries.valuation_sub_toLaurentSeries_trunc_le: the valuation bound on truncation errors.
• TauCeti.LaurentSeries.continuousLinearMap_ext_single: continuous linear maps into a Hausdorff module are determined by their values on monomials.

noncomputable def LaurentPolynomial.toLaurentSeries {R : Type u_1} [Semiring R] : LaurentPolynomial R →+* LaurentSeries R

The inclusion of Laurent polynomials into Laurent series, sending T to X.

@[simp]

theorem LaurentPolynomial.toLaurentSeries_T {R : Type u_1} [Semiring R] (n : ℤ) : toLaurentSeries (T n) = (HahnSeries.single n) 1

Tⁿ is sent to Xⁿ, for every integer n.

theorem LaurentPolynomial.toLaurentSeries_single {R : Type u_1} [Semiring R] (n : ℤ) (a : R) : toLaurentSeries (AddMonoidAlgebra.single n a) = (HahnSeries.single n) a

The monomial a Tⁿ is sent to a Xⁿ.

@[simp]

theorem LaurentPolynomial.toLaurentSeries_C {R : Type u_1} [Semiring R] (r : R) : toLaurentSeries (C r) = HahnSeries.C r

Constants are sent to constants.

@[simp]

theorem LaurentPolynomial.toLaurentSeries_toLaurent {R : Type u_1} [Semiring R] (p : Polynomial R) : toLaurentSeries (Polynomial.toLaurent p) = (HahnSeries.ofPowerSeries ℤ R) ↑p

The inclusion of a polynomial into Laurent series agrees with first viewing it as a Laurent polynomial.

@[simp]

theorem LaurentPolynomial.coeff_toLaurentSeries {R : Type u_1} [Semiring R] (p : LaurentPolynomial R) (n : ℤ) : (toLaurentSeries p).coeff n = p.coeff n

The inclusion of Laurent polynomials into Laurent series preserves coefficients.

theorem LaurentPolynomial.toLaurentSeries_injective {R : Type u_1} [Semiring R] : Function.Injective ⇑toLaurentSeries

The inclusion of Laurent polynomials into Laurent series is injective.

@[simp]

theorem LaurentPolynomial.support_toLaurentSeries {R : Type u_1} [Semiring R] (p : LaurentPolynomial R) : HahnSeries.support (toLaurentSeries p) = ↑p.coeff.support

The support of a Laurent polynomial viewed as a Laurent series is its finite support.

theorem LaurentPolynomial.mem_range_toLaurentSeries_iff {R : Type u_1} [Semiring R] (f : LaurentSeries R) : f ∈ Set.range ⇑toLaurentSeries ↔ (HahnSeries.support f).Finite

A Laurent series is the image of a Laurent polynomial exactly when it has finite support.

theorem LaurentPolynomial.order_toLaurentSeries {R : Type u_1} [Semiring R] (p : LaurentPolynomial R) (hp : p ≠ 0) : HahnSeries.order (toLaurentSeries p) = p.coeff.support.min' ⋯

The order of a nonzero Laurent polynomial viewed as a Laurent series is the least exponent in its support.

@[simp]

theorem LaurentPolynomial.toLaurentSeries_derivative {R : Type u_1} [Ring R] (p : LaurentPolynomial R) : toLaurentSeries (derivative p) = (LaurentSeries.derivative R) (toLaurentSeries p)

The inclusion of Laurent polynomials into Laurent series commutes with differentiation.

@[instance_reducible]

noncomputable instance LaurentSeries.algebraLaurentPolynomial {R : Type u_1} [CommSemiring R] : Algebra (LaurentPolynomial R) (LaurentSeries R)

Laurent series form an algebra over Laurent polynomials through the finite-support inclusion.

@[simp]

theorem LaurentPolynomial.algebraMap_eq_toLaurentSeries {R : Type u_1} [CommSemiring R] (p : LaurentPolynomial R) : (algebraMap (LaurentPolynomial R) (LaurentSeries R)) p = toLaurentSeries p

The algebra map from Laurent polynomials to Laurent series is the finite-support inclusion.

instance LaurentPolynomial.isScalarTower_laurentSeries {R : Type u_1} [CommSemiring R] : IsScalarTower R (LaurentPolynomial R) (LaurentSeries R)

The coefficient ring, Laurent-polynomial ring, and Laurent-series ring form an algebra tower.

instance LaurentPolynomial.isScalarTower_polynomial_laurentPolynomial {R : Type u_1} [CommSemiring R] : IsScalarTower (Polynomial R) (LaurentPolynomial R) (LaurentSeries R)

The polynomial, Laurent-polynomial, and Laurent-series algebra structures form a tower.

theorem LaurentSeries.finite_support_truncLT {A : Type u_1} [Zero A] (a : ℤ) (f : LaurentSeries A) : (Function.support ((HahnSeries.truncLT a) f).coeff).Finite

Truncating a Laurent series below an integer cutoff gives finite support.

noncomputable def LaurentSeries.trunc {R : Type u_1} [Semiring R] (N : ℤ) : LaurentSeries R →ₗ[R] LaurentPolynomial R

The Laurent polynomial obtained from a Laurent series by retaining the coefficients at exponents strictly less than N. The lower bound on a Laurent series makes this a finite sum.

@[simp]

theorem LaurentSeries.coeff_trunc {R : Type u_1} [Semiring R] (N n : ℤ) (f : LaurentSeries R) : ((trunc N) f).coeff n = if n < N then f.coeff n else 0

The coefficient of a truncation agrees with the original series below the cutoff and vanishes at and above it.

@[simp]

theorem LaurentSeries.toLaurentSeries_trunc {R : Type u_1} [Semiring R] (N : ℤ) (f : LaurentSeries R) : LaurentPolynomial.toLaurentSeries ((trunc N) f) = (HahnSeries.truncLT N) f

Embedding a Laurent-polynomial truncation gives the corresponding strict truncation of the Hahn series.

theorem LaurentSeries.trunc_eq_sum_Ico {R : Type u_1} [Semiring R] (N : ℤ) (f : LaurentSeries R) : (trunc N) f = ∑ j ∈ Finset.Ico (HahnSeries.order f) N, AddMonoidAlgebra.single j (f.coeff j)

A Laurent truncation is the finite sum of its monomials between the order of the series and the cutoff. This also holds when the cutoff lies below the order, giving an empty sum.

theorem LaurentSeries.le_orderTop_sub_toLaurentSeries_trunc {A : Type u_2} [Ring A] (N : ℤ) (f : LaurentSeries A) : ↑N ≤ HahnSeries.orderTop (LaurentPolynomial.toLaurentSeries ((trunc N) f) - f)

The difference between a Laurent series and its truncation has order at least the cutoff.

theorem LaurentSeries.tendsto_toLaurentSeries_trunc {K : Type u_2} [Field K] (f : LaurentSeries K) : Filter.Tendsto (fun (N : ℤ) => LaurentPolynomial.toLaurentSeries ((trunc N) f)) Filter.atTop (nhds f)

The Laurent-polynomial truncations of a Laurent series converge to it in the valuation topology.

theorem LaurentSeries.valuation_sub_toLaurentSeries_trunc_le {K : Type u_2} [Field K] (a : ℤ) (f : LaurentSeries K) : Valued.v (f - LaurentPolynomial.toLaurentSeries ((trunc a) f)) ≤ WithZero.exp (-a)

The truncation error has valuation at most exp (-a).

theorem LaurentPolynomial.denseRange_toLaurentSeries {K : Type u_1} [Field K] : DenseRange ⇑toLaurentSeries

Laurent polynomials are dense in the Laurent-series field for the valuation topology.

theorem TauCeti.LaurentSeries.continuousLinearMap_ext_single {K : Type u_1} {M : Type u_2} [Field K] [AddCommMonoid M] [Module K M] [TopologicalSpace M] [T2Space M] {ℓ m : LaurentSeries K →L[K] M} (h : ∀ (n : ℤ), ℓ ((HahnSeries.single n) 1) = m ((HahnSeries.single n) 1)) : ℓ = m

Continuous linear maps from a Laurent-series field to a Hausdorff module are determined by their values on the monomials with coefficient one.

theorem TauCeti.LaurentSeries.continuousLinearMap_ext_single_iff {K : Type u_1} {M : Type u_2} [Field K] [AddCommMonoid M] [Module K M] [TopologicalSpace M] [T2Space M] {ℓ m : LaurentSeries K →L[K] M} : ℓ = m ↔ ∀ (n : ℤ), ℓ ((HahnSeries.single n) 1) = m ((HahnSeries.single n) 1)