Laurent Series #

In this file we define LaurentSeries R, the formal Laurent series over R, here an arbitrary type with a zero. They are denoted R⸨X⸩.

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 from power series R⟦X⟧ into R⸨X⸩ 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
In LaurentSeries.uniformContinuous_coeff we show that sending a Laurent series to its dth coefficient is uniformly continuous, ensuring that it sends a Cauchy filter ℱ in K⸨X⸩ to a Cauchy filter in K: since this latter is given the discrete topology, this provides an element LaurentSeries.Cauchy.coeff ℱ d in K that serves as dth coefficient of the Laurent series to which the filter ℱ converges.

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 LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero.
The valuation of a Laurent series is the order of the first non-zero coefficient, see LaurentSeries.valuation_le_iff_coeff_lt_eq_zero.
Every Laurent series of valuation less than (1 : ℤᵐ⁰) comes from a power series, see LaurentSeries.val_le_one_iff_eq_coe.
The uniform space of LaurentSeries over a field is complete, formalized in the instance instLaurentSeriesComplete.
The field of rational functions is dense in LaurentSeries: this is the declaration LaurentSeries.coe_range_dense and relies principally upon LaurentSeries.exists_ratFunc_val_lt, stating that for every Laurent series f and every γ : ℤᵐ⁰ one can find a rational function Q such that the X-adic valuation v satisfies v (f - Q) < γ.
In LaurentSeries.valuation_compare we prove that the extension of the X-adic valuation from K⟮X⟯ up to its abstract completion coincides, modulo the isomorphism with K⸨X⸩, with the X-adic valuation on K⸨X⸩.
The two declarations LaurentSeries.mem_integers_of_powerSeries and LaurentSeries.exists_powerSeries_of_memIntegers show that an element in the completion of K⟮X⟯ is in the unit ball if and only if it comes from a power series through the isomorphism LaurentSeriesRingEquiv.
LaurentSeries.powerSeriesAlgEquiv is the K-algebra isomorphism between K⟦X⟧ and the unit ball inside the X-adic completion of K⟮X⟯.

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 : R⸨X⸩ to single 1 1 : R⟦ℤ⟧.
To prove the isomorphism between the X-adic completion of K⟮X⟯ and K⸨X⸩ we construct two completions of K⟮X⟯: the first (LaurentSeries.ratfuncAdicComplPkg) is its abstract uniform completion; the second (LaurentSeries.LaurentSeriesPkg) is simply K⸨X⸩, once we prove that it is complete and contains K⟮X⟯ as a dense subspace. The isomorphism is the comparison equivalence, expressing the mathematical idea that the completion "is unique". It is LaurentSeries.comparePkg.
For applications to K⟦X⟧ it is actually more handy to use the inverse of the above equivalence: LaurentSeries.LaurentSeriesAlgEquiv is the topological, algebra equivalence K⸨X⸩ ≃ₐ[K] RatFuncAdicCompl K.
In order to compare K⟦X⟧ with the valuation subring in the X-adic completion of K⟮X⟯ we consider its alias LaurentSeries.powerSeries_as_subring as a subring of K⸨X⸩, that is itself clearly isomorphic (via the inverse of LaurentSeries.powerSeriesEquivSubring) to K⟦X⟧.

source

@[reducible, inline]

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

Type u

LaurentSeries R is the type of formal Laurent series with coefficients in R, denoted R⸨X⸩.

It is implemented as a HahnSeries with value group ℤ.

Equations

LaurentSeries R = HahnSeries ℤ R

Instances For

source

def LaurentSeries.«term_⸨X⸩» :

Lean.TrailingParserDescr

R⸨X⸩ is notation for LaurentSeries R.

Equations

LaurentSeries.«term_⸨X⸩» = Lean.ParserDescr.trailingNode `LaurentSeries.«term_⸨X⸩» 9000 0 (Lean.ParserDescr.symbol "⸨X⸩")

Instances For

source

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.

Instances For

source

@[simp]

theorem LaurentSeries.hasseDeriv_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) (n : ℤ) :

((hasseDeriv R k) f).coeff n = Ring.choose (n + ↑k) k • f.coeff (n + ↑k)

source

@[simp]

theorem LaurentSeries.hasseDeriv_zero {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] :

hasseDeriv R 0 = LinearMap.id

source

theorem LaurentSeries.hasseDeriv_single_add {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (n : ℤ) (x : V) :

(hasseDeriv R k) ((HahnSeries.single (n + ↑k)) x) = (HahnSeries.single n) (Ring.choose (n + ↑k) k • x)

source

@[simp]

theorem LaurentSeries.hasseDeriv_single {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (n : ℤ) (x : V) :

(hasseDeriv R k) ((HahnSeries.single n) x) = (HahnSeries.single (n - ↑k)) (Ring.choose n k • x)

source

theorem LaurentSeries.hasseDeriv_comp_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k l : ℕ) (f : LaurentSeries V) (n : ℤ) :

((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

source

@[simp]

theorem LaurentSeries.hasseDeriv_comp {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k l : ℕ) (f : LaurentSeries V) :

(hasseDeriv R k) ((hasseDeriv R l) f) = (k + l).choose k • (hasseDeriv R (k + l)) f

source

def LaurentSeries.derivative (R : Type u_3) {V : Type u_4} [AddCommGroup V] [Semiring R] [Module R V] :

LaurentSeries V →ₗ[R] LaurentSeries V

The derivative of a Laurent series.

Equations

LaurentSeries.derivative R = LaurentSeries.hasseDeriv R 1

Instances For

source

@[simp]

theorem LaurentSeries.derivative_apply {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (f : LaurentSeries V) :

(derivative R) f = (hasseDeriv R 1) f

source

theorem LaurentSeries.derivative_iterate {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) :

(⇑(derivative R))^[k] f = k.factorial • (hasseDeriv R k) f

source

@[simp]

theorem LaurentSeries.derivative_iterate_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) (n : ℤ) :

((⇑(derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instCoePowerSeries {R : Type u_1} [Semiring R] :

Coe (PowerSeries R) (LaurentSeries R)

Equations

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

source

@[simp]

theorem LaurentSeries.coeff_coe_powerSeries {R : Type u_1} [Semiring R] (x : PowerSeries R) (n : ℕ) :

((HahnSeries.ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff n) x

source

noncomputable 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)

Instances For

source

@[simp]

theorem LaurentSeries.powerSeriesPart_coeff {R : Type u_1} [Semiring R] (x : LaurentSeries R) (n : ℕ) :

(PowerSeries.coeff n) x.powerSeriesPart = x.coeff (HahnSeries.order x + ↑n)

source

@[simp]

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

powerSeriesPart 0 = 0

source

@[simp]

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

x.powerSeriesPart = 0 ↔ x = 0

source

@[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

source

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

source

theorem LaurentSeries.X_order_mul_powerSeriesPart {R : Type u_1} [Semiring R] {n : ℕ} {f : LaurentSeries R} (hn : ↑n = HahnSeries.order f) :

(HahnSeries.ofPowerSeries ℤ R) (PowerSeries.X ^ n * f.powerSeriesPart) = f

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instAlgebraPowerSeries {R : Type u_1} [CommSemiring R] :

Algebra (PowerSeries R) (LaurentSeries R)

Equations

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

source

@[simp]

theorem LaurentSeries.coe_algebraMap {R : Type u_1} [CommSemiring R] :

⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = ⇑(HahnSeries.ofPowerSeries ℤ R)

source

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.

source

instance LaurentSeries.instIsFractionRingPowerSeries {K : Type u_2} [Field K] :

IsFractionRing (PowerSeries K) (LaurentSeries K)

source

theorem PowerSeries.coe_zero {R : Type u_1} [Semiring R] :

(HahnSeries.ofPowerSeries ℤ R) 0 = 0

source

theorem PowerSeries.coe_one {R : Type u_1} [Semiring R] :

(HahnSeries.ofPowerSeries ℤ R) 1 = 1

source

theorem PowerSeries.coe_add {R : Type u_1} [Semiring R] (f g : PowerSeries R) :

(HahnSeries.ofPowerSeries ℤ R) (f + g) = (HahnSeries.ofPowerSeries ℤ R) f + (HahnSeries.ofPowerSeries ℤ R) g

source

theorem PowerSeries.coe_sub {R' : Type u_2} [Ring R'] (f' g' : PowerSeries R') :

(HahnSeries.ofPowerSeries ℤ R') (f' - g') = (HahnSeries.ofPowerSeries ℤ R') f' - (HahnSeries.ofPowerSeries ℤ R') g'

source

theorem PowerSeries.coe_neg {R' : Type u_2} [Ring R'] (f' : PowerSeries R') :

(HahnSeries.ofPowerSeries ℤ R') (-f') = -(HahnSeries.ofPowerSeries ℤ R') f'

source

theorem PowerSeries.coe_mul {R : Type u_1} [Semiring R] (f g : PowerSeries R) :

(HahnSeries.ofPowerSeries ℤ R) (f * g) = (HahnSeries.ofPowerSeries ℤ R) f * (HahnSeries.ofPowerSeries ℤ R) g

source

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 (coeff i.natAbs) f

source

theorem PowerSeries.coe_C {R : Type u_1} [Semiring R] (r : R) :

(HahnSeries.ofPowerSeries ℤ R) (C r) = HahnSeries.C r

source

theorem PowerSeries.coe_X {R : Type u_1} [Semiring R] :

(HahnSeries.ofPowerSeries ℤ R) X = (HahnSeries.single 1) 1

source

@[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

source

theorem PowerSeries.coe_pow {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) :

(HahnSeries.ofPowerSeries ℤ R) (f ^ n) = (HahnSeries.ofPowerSeries ℤ R) f ^ n

source

instance RatFunc.instFaithfulSMulPolynomialLaurentSeries {F : Type u} [Field F] :

FaithfulSMul (Polynomial F) (LaurentSeries F)

source

@[implicit_reducible]

noncomputable instance RatFunc.coeToLaurentSeries {F : Type u} [Field F] :

Coe (RatFunc F) (LaurentSeries F)

Equations

RatFunc.coeToLaurentSeries = { coe := ⇑(algebraMap (RatFunc F) (LaurentSeries F)) }

source

theorem RatFunc.coe_coe {F : Type u} [Field F] (P : Polynomial F) :

(HahnSeries.ofPowerSeries ℤ F) ↑P = (algebraMap (RatFunc F) (LaurentSeries F)) ↑P

source

@[simp]

theorem RatFunc.coe_X {F : Type u} [Field F] :

(algebraMap (RatFunc F) (LaurentSeries F)) X = (HahnSeries.single 1) 1

source

theorem RatFunc.single_one_eq_pow {R : Type u_2} [Semiring R] (n : ℕ) :

(HahnSeries.single ↑n) 1 = (HahnSeries.single 1) 1 ^ n

source

theorem RatFunc.single_zpow {F : Type u} [Field F] (n : ℤ) :

(HahnSeries.single n) 1 = (HahnSeries.single 1) 1 ^ n

source

theorem RatFunc.algebraMap_apply_div {F : Type u} [Field F] (p 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

source

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

IsDedekindDomain.HeightOneSpectrum (PowerSeries K)

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

Equations

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

Instances For

source

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

(Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

source

@[simp]

theorem PowerSeries.intValuation_X {K : Type u_2} [Field K] :

(idealX K).intValuation X = WithZero.exp (-1)

The integral valuation of the power series X : K⟦X⟧ equals (ofAdd -1) : ℤᵐ⁰.

source

@[reducible, inline]

noncomputable abbrev RatFunc.polynomialValuationX (K : Type u_2) [Field K] :

Valuation (RatFunc K) (WithZero (Multiplicative ℤ))

polynomialValuationX is an abbreviation for the X-adic valuation given by (Polynomial.idealX K).valuation K⟮X⟯.

Equations

RatFunc.polynomialValuationX K = IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)

Instances For

source

theorem RatFunc.valuation_eq_LaurentSeries_valuation (K : Type u_2) [Field K] (P : RatFunc K) :

(polynomialValuationX K) P = (IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K)) ((algebraMap (RatFunc K) (LaurentSeries K)) P)

source

@[implicit_reducible]

noncomputable instance LaurentSeries.valued (K : Type u_2) [Field K] :

Valued (LaurentSeries K) (WithZero (Multiplicative ℤ))

Equations

LaurentSeries.valued K = Valued.mk' (IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K))

source

theorem LaurentSeries.valuation_def (K : Type u_2) [Field K] :

Valued.v = IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K)

source

theorem LaurentSeries.valuation_coe_ratFunc (K : Type u_2) [Field K] (f : RatFunc K) :

Valued.v ((algebraMap (RatFunc K) (LaurentSeries K)) f) = Valued.v f

source

theorem LaurentSeries.valuation_X_pow (K : Type u_2) [Field K] (s : ℕ) :

Valued.v ((HahnSeries.ofPowerSeries ℤ K) PowerSeries.X ^ s) = WithZero.exp (-↑s)

source

theorem LaurentSeries.valuation_single_zpow (K : Type u_2) [Field K] (s : ℤ) :

Valued.v ((HahnSeries.single s) 1) = WithZero.exp (-s)

source

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) ≤ WithZero.exp (-↑d)) :

n < d → (PowerSeries.coeff n) f = 0

source

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) ≤ WithZero.exp (-↑d) ↔ ∀ n < d, (PowerSeries.coeff n) f = 0

source

theorem LaurentSeries.coeff_zero_of_lt_valuation (K : Type u_2) [Field K] {n D : ℤ} {f : LaurentSeries K} (H : Valued.v f ≤ WithZero.exp (-D)) :

n < D → f.coeff n = 0

The coefficients of a Laurent series vanish in degree strictly less than its valuation.

source

theorem LaurentSeries.valuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {D : ℤ} {f : LaurentSeries K} :

Valued.v f ≤ WithZero.exp (-D) ↔ ∀ n < D, f.coeff n = 0

The valuation of a Laurent series is the order of the first non-zero coefficient.

source

theorem LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero (K : Type u_2) [Field K] {D : WithZero (Multiplicative ℤ)} (hD : D ≠ 0) {f : LaurentSeries K} :

Valued.v f ≤ D ↔ ∀ n < -D.log, f.coeff n = 0

source

theorem LaurentSeries.eq_coeff_of_valuation_sub_lt (K : Type u_2) [Field K] {d n : ℤ} {f g : LaurentSeries K} (H : Valued.v (g - f) ≤ WithZero.exp (-d)) :

n < d → g.coeff n = f.coeff n

Two Laurent series whose difference has small valuation have the same coefficients for small enough indices.

source

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

Every Laurent series of valuation less than (1 : ℤᵐ⁰) comes from a power series.

source

theorem LaurentSeries.valuation_surjective (K : Type u_2) [Field K] :

Function.Surjective ⇑Valued.v

source

theorem LaurentSeries.uniformContinuous_coeff {K : Type u_2} [Field K] {uK : UniformSpace K} (d : ℤ) :

UniformContinuous fun (f : LaurentSeries K) => f.coeff d

Sending a Laurent series to its d-th coefficient is uniformly continuous (independently of the uniformity with which K is endowed).

source

noncomputable def LaurentSeries.Cauchy.coeff {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :

ℤ → K

Since extracting coefficients is uniformly continuous, every Cauchy filter in K⸨X⸩ gives rise to a Cauchy filter in K for every d : ℤ, and such Cauchy filter in K converges to a principal filter

Equations

LaurentSeries.Cauchy.coeff hℱ = fun (d : ℤ) => DiscreteUniformity.cauchyConst ⋯

Instances For

source

theorem LaurentSeries.Cauchy.coeff_tendsto {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) (D : ℤ) :

Filter.Tendsto (fun (f : LaurentSeries K) => f.coeff D) ℱ (Filter.principal {coeff hℱ D})

source

theorem LaurentSeries.Cauchy.exists_lb_eventual_support {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :

∃ (N : ℤ), ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ n < N, f.coeff n = 0

source

theorem LaurentSeries.Cauchy.exists_lb_support {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :

∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0

The support of Cauchy.coeff has a lower bound.

source

theorem LaurentSeries.Cauchy.coeff_support_bddBelow {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :

BddBelow (Function.support (coeff hℱ))

The support of Cauchy.coeff is bounded below

source

noncomputable def LaurentSeries.Cauchy.limit {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :

LaurentSeries K

To any Cauchy filter ℱ of K⸨X⸩, we can attach a laurent series that is the limit of the filter. Its d-th coefficient is defined as the limit of Cauchy.coeff hℱ d, which is again Cauchy but valued in the discrete space K. That sufficiently negative coefficients vanish follows from Cauchy.coeff_support_bddBelow

Equations

LaurentSeries.Cauchy.limit hℱ = { coeff := LaurentSeries.Cauchy.coeff hℱ, isPWO_support' := ⋯ }

Instances For

source

theorem LaurentSeries.Cauchy.exists_lb_coeff_ne {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :

∃ (N : ℤ), ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

The following lemma shows that for every d smaller than the minimum between the integers produced in Cauchy.exists_lb_eventual_support and Cauchy.exists_lb_support, for almost all series in ℱ the dth coefficient coincides with the dth coefficient of Cauchy.coeff hℱ.

source

theorem LaurentSeries.Cauchy.coeff_eventually_equal {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {D : ℤ} :

∀ᶠ (f : LaurentSeries K) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Given a Cauchy filter ℱ in the Laurent Series and a bound D, for almost all series in the filter the coefficients below D coincide with Cauchy.coeff hℱ.

source

theorem LaurentSeries.Cauchy.eventually_mem_nhds {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {U : Set (LaurentSeries K)} (hU : U ∈ nhds (limit hℱ)) :

∀ᶠ (f : LaurentSeries K) in ℱ, f ∈ U

The main result showing that the Cauchy filter tends to the Cauchy.limit

source

instance LaurentSeries.instLaurentSeriesComplete {K : Type u_2} [Field K] :

CompleteSpace (LaurentSeries K)

Laurent Series with coefficients in a field are complete w.r.t. the X-adic valuation

source

theorem LaurentSeries.exists_Polynomial_intValuation_lt {K : Type u_2} [Field K] (F : PowerSeries K) (η : (WithZero (Multiplicative ℤ))ˣ) :

∃ (P : Polynomial K), (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

source

theorem LaurentSeries.exists_ratFunc_val_lt {K : Type u_2} [Field K] (f : LaurentSeries K) (γ : (WithZero (Multiplicative ℤ))ˣ) :

∃ (Q : RatFunc K), Valued.v (f - (algebraMap (RatFunc K) (LaurentSeries K)) Q) < ↑γ

For every Laurent series f and every γ : ℤᵐ⁰ one can find a rational function Q such that the X-adic valuation v satisfies v (f - Q) < γ.

source

theorem LaurentSeries.coe_range_dense {K : Type u_2} [Field K] :

DenseRange ⇑(algebraMap (RatFunc K) (LaurentSeries K))

source

theorem LaurentSeries.exists_ratFunc_eq_v {K : Type u_2} [Field K] (x : LaurentSeries K) :

∃ (f : RatFunc K), Valued.v f = Valued.v x

source

theorem LaurentSeries.inducing_coe {K : Type u_2} [Field K] :

IsUniformInducing ⇑(algebraMap (RatFunc K) (LaurentSeries K))

source

theorem LaurentSeries.uniformContinuous_withVal_equiv {K : Type u_2} [Field K] :

UniformContinuous ⇑(WithVal.equiv (RatFunc.polynomialValuationX K))

source

theorem LaurentSeries.continuous_coe {K : Type u_2} [Field K] :

Continuous ⇑(algebraMap (RatFunc K) (LaurentSeries K))

source

@[reducible, inline]

noncomputable abbrev LaurentSeries.ratfuncAdicComplPkg {K : Type u_2} [Field K] :

AbstractCompletion.{u_2, u_2} (WithVal (RatFunc.polynomialValuationX K))

The X-adic completion as an abstract completion of K⟮X⟯

Equations

LaurentSeries.ratfuncAdicComplPkg = UniformSpace.Completion.cPkg

Instances For

source

noncomputable def LaurentSeries.LaurentSeriesPkg (K : Type u_2) [Field K] :

AbstractCompletion.{u_2, u_2} (WithVal (RatFunc.polynomialValuationX K))

Having established that the K⸨X⸩ is complete and contains K⟮X⟯ as a dense subspace, it gives rise to an abstract completion of K⟮X⟯.

Equations

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

Instances For

source

theorem LaurentSeries.continuous_coe' (K : Type u_2) [Field K] :

Continuous (⇑(algebraMap (RatFunc K) (LaurentSeries K)) ∘ ⇑(WithVal.equiv (RatFunc.polynomialValuationX K)))

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instTopologicalSpaceSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXLaurentSeriesPkg (K : Type u_2) [Field K] :

TopologicalSpace (LaurentSeriesPkg K).space

Equations

LaurentSeries.instTopologicalSpaceSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXLaurentSeriesPkg K = (LaurentSeries.LaurentSeriesPkg K).uniformStruct.toTopologicalSpace

source

@[simp]

theorem LaurentSeries.LaurentSeries_coe (K : Type u_2) [Field K] (x : RatFunc K) :

(LaurentSeriesPkg K).coe (WithVal.toVal (RatFunc.polynomialValuationX K) x) = (algebraMap (RatFunc K) (LaurentSeries K)) x

source

@[reducible, inline]

noncomputable abbrev LaurentSeries.extensionAsRingHom (K : Type u_2) [Field K] (hf : Continuous ⇑((algebraMap (RatFunc K) (LaurentSeries K)).comp (WithVal.equiv (RatFunc.polynomialValuationX K)).toRingHom)) [CompleteSpace (LaurentSeries K)] [T0Space (LaurentSeries K)] :

UniformSpace.Completion (WithVal (RatFunc.polynomialValuationX K)) →+* LaurentSeries K

Reinterpret the extension of coe : WithVal ((idealX K).valuation _) → K⸨X⸩ as a ring homomorphism

Equations

LaurentSeries.extensionAsRingHom K = UniformSpace.Completion.extensionHom ((algebraMap (RatFunc K) (LaurentSeries K)).comp (WithVal.equiv (RatFunc.polynomialValuationX K)).toRingHom)

Instances For

source

@[reducible, inline]

abbrev LaurentSeries.RatFuncAdicCompl (K : Type u_2) [Field K] :

Type u_2

An abbreviation for the X-adic completion of K⟮X⟯

Equations

LaurentSeries.RatFuncAdicCompl K = IsDedekindDomain.HeightOneSpectrum.adicCompletion (RatFunc K) (Polynomial.idealX K)

Instances For

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instFieldSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXRatfuncAdicComplPkg (K : Type u_2) [Field K] :

Field ratfuncAdicComplPkg.space

Equations

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

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instValuedSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXRatfuncAdicComplPkg (K : Type u_2) [Field K] :

Valued ratfuncAdicComplPkg.space (WithZero (Multiplicative ℤ))

Equations

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

The two instances below make comparePkg and comparePkg_eq_extension slightly faster.

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instUniformSpaceRatFuncAdicCompl (K : Type u_2) [Field K] :

UniformSpace (RatFuncAdicCompl K)

Equations

LaurentSeries.instUniformSpaceRatFuncAdicCompl K = inferInstance

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instUniformSpace (K : Type u_2) [Field K] :

UniformSpace (LaurentSeries K)

Equations

LaurentSeries.instUniformSpace K = inferInstance

source

@[reducible, inline]

noncomputable abbrev LaurentSeries.comparePkg (K : Type u_2) [Field K] :

RatFuncAdicCompl K ≃ᵤ LaurentSeries K

The uniform space isomorphism between two abstract completions of ratfunc K

Equations

LaurentSeries.comparePkg K = LaurentSeries.ratfuncAdicComplPkg.compareEquiv (LaurentSeries.LaurentSeriesPkg K)

Instances For

source

theorem LaurentSeries.comparePkg_eq_extension (K : Type u_2) [Field K] (x : RatFuncAdicCompl K) :

(comparePkg K) x = (extensionAsRingHom K ⋯) x

source

@[reducible, inline]

noncomputable abbrev LaurentSeries.ratfuncAdicComplRingEquiv (K : Type u_2) [Field K] :

RatFuncAdicCompl K ≃+* LaurentSeries K

The uniform space equivalence between two abstract completions of ratfunc K as a ring equivalence: this will be the inverse of the fundamental one.

Equations

LaurentSeries.ratfuncAdicComplRingEquiv K = { toEquiv := (LaurentSeries.comparePkg K).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[reducible, inline]

noncomputable abbrev LaurentSeries.LaurentSeriesRingEquiv (K : Type u_2) [Field K] :

LaurentSeries K ≃+* RatFuncAdicCompl K

The uniform space equivalence between two abstract completions of ratfunc K as a ring equivalence: it goes from K⸨X⸩ to RatFuncAdicCompl K

Equations

LaurentSeries.LaurentSeriesRingEquiv K = (LaurentSeries.ratfuncAdicComplRingEquiv K).symm

Instances For

source

theorem LaurentSeries.LaurentSeriesRingEquiv_def (K : Type u_2) [Field K] (f : PowerSeries K) :

(LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f) = (LaurentSeriesPkg K).compare ratfuncAdicComplPkg ((HahnSeries.ofPowerSeries ℤ K) f)

source

@[simp]

theorem LaurentSeries.ratfuncAdicComplRingEquiv_apply (K : Type u_2) [Field K] (x : RatFuncAdicCompl K) :

(ratfuncAdicComplRingEquiv K) x = ratfuncAdicComplPkg.compare (LaurentSeriesPkg K) x

source

theorem LaurentSeries.coe_X_compare (K : Type u_2) [Field K] :

(ratfuncAdicComplRingEquiv K) ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K))).symm RatFunc.X) = (HahnSeries.ofPowerSeries ℤ K) PowerSeries.X

source

theorem LaurentSeries.algebraMap_apply (K : Type u_2) [Field K] (a : K) :

(algebraMap K (LaurentSeries K)) a = HahnSeries.C a

source

@[implicit_reducible]

noncomputable instance LaurentSeries.instAlgebraRatFuncAdicCompl (K : Type u_2) [Field K] :

Algebra K (RatFuncAdicCompl K)

Equations

LaurentSeries.instAlgebraRatFuncAdicCompl K = ((LaurentSeries.LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C).toAlgebra

source

noncomputable def LaurentSeries.LaurentSeriesAlgEquiv (K : Type u_2) [Field K] :

LaurentSeries K ≃ₐ[K] RatFuncAdicCompl K

The algebra equivalence between K⸨X⸩ and the X-adic completion of RatFunc X

Equations

LaurentSeries.LaurentSeriesAlgEquiv K = AlgEquiv.ofRingEquiv ⋯

Instances For

source

theorem LaurentSeries.valuation_LaurentSeries_equal_extension (K : Type u_2) [Field K] :

⋯.extend ⇑Valued.v = ⇑Valued.v

source

theorem LaurentSeries.tendsto_valuation (K : Type u_2) [Field K] (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion (RatFunc K) (Polynomial.idealX K)) :

Filter.Tendsto (⇑Valued.v) (Filter.comap (fun (x : RatFunc K) => ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K))).symm x)) (nhds a)) (nhds (Valued.v a))

source

theorem LaurentSeries.valuation_compare (K : Type u_2) [Field K] (f : LaurentSeries K) :

Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f

The extension of the X-adic valuation from K⟮X⟯ up to its abstract completion coincides, modulo the isomorphism with K⸨X⸩, with the X-adic valuation on K⸨X⸩.

source

@[reducible, inline]