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 RatFunc K 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 RatFunc K 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 RatFunc K.

Implementation details #

Since LaurentSeries is just an abbreviation of HahnSeries ℤ R, 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 : HahnSeries ℤ R.
To prove the isomorphism between the X-adic completion of RatFunc K and K⸨X⸩ we construct two completions of RatFunc K: 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 RatFunc K 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 RatFunc K 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

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⸩")

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.

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

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

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 R n) x

source

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)

source

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

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

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

source

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

(HahnSeries.ofPowerSeries ℤ R) ((C R) 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

def RatFunc.coeAlgHom (F : Type u) [Field F] :

RatFunc F →ₐ[Polynomial F] LaurentSeries F

The coercion RatFunc F → F⸨X⸩ as bundled alg hom.

Equations

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

source

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

RatFunc F → LaurentSeries F

The coercion RatFunc F → F⸨X⸩ as a function.

This is the implementation of coeToLaurentSeries.

Equations

RatFunc.coeToLaurentSeries_fun = ⇑(RatFunc.coeAlgHom F)

source

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

Coe (RatFunc F) (LaurentSeries F)

Equations

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

source

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

↑f = (coeAlgHom F) f

source

theorem RatFunc.coe_num_denom {F : Type u} [Field F] (f : RatFunc F) :

↑f = (HahnSeries.ofPowerSeries ℤ F) ↑f.num / (HahnSeries.ofPowerSeries ℤ F) ↑f.denom

source

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

Function.Injective coeToLaurentSeries_fun

source

@[simp]

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

(coeAlgHom F) f = ↑f

source

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

(HahnSeries.ofPowerSeries ℤ F) ↑P = ↑↑P

source

@[simp]

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

↑0 = 0

source

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

↑f ≠ 0

source

@[simp]

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

↑1 = 1

source

@[simp]

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

↑(f + g) = ↑f + ↑g

source

@[simp]

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

↑(f - g) = ↑f - ↑g

source

@[simp]

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

↑(-f) = -↑f

source

@[simp]

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

↑(f * g) = ↑f * ↑g

source

@[simp]

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

↑(f ^ n) = ↑f ^ n

source

@[simp]

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

↑(f / g) = ↑f / ↑g

source

@[simp]

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

↑(C r) = HahnSeries.C r

source

@[simp]

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

↑(r • f) = r • ↑f

source

@[simp]

theorem RatFunc.coe_X {F : Type u} [Field 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_inv {F : Type u} [Field F] (d : ℤ) {α : F} (hα : α ≠ 0) :

(HahnSeries.single (-d)) α⁻¹ = ((HahnSeries.single d) α)⁻¹

source

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

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

source

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

Algebra (RatFunc F) (LaurentSeries F)

Equations

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

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

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

IsScalarTower (Polynomial F) (RatFunc F) (LaurentSeries F)

source

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 := ⋯ }

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 = ↑(Multiplicative.ofAdd (-1))

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

source

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

(IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)) P = (IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K)) ↑P

source

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

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

Equations

LaurentSeries.instValuedWithZeroMultiplicativeInt 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_X_pow (K : Type u_2) [Field K] (s : ℕ) :

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

source

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

Valued.v ((HahnSeries.single s) 1) = ↑(Multiplicative.ofAdd (-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) ≤ ↑(Multiplicative.ofAdd (-↑d))) :

n < d → (PowerSeries.coeff K 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) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K 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 ≤ ↑(Multiplicative.ofAdd (-D))) :

n < D → f.coeff n = 0

source

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

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) ≤ ↑(Multiplicative.ofAdd (-d))) :

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

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

source

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

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

source

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 ⋯

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

source

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

BddBelow (Function.support (coeff hℱ))

source

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' := ⋯ }

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

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

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

source

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

CompleteSpace (LaurentSeries K)

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 - ↑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 RatFunc.coeToLaurentSeries_fun

source

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

IsUniformInducing RatFunc.coeToLaurentSeries_fun

source

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

Continuous RatFunc.coeToLaurentSeries_fun

source

@[reducible, inline]

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

AbstractCompletion (RatFunc K)

The X-adic completion as an abstract completion of RatFunc K

Equations

LaurentSeries.ratfuncAdicComplPkg = UniformSpace.Completion.cPkg

source

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

AbstractCompletion (RatFunc K)

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

Equations

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

source

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

TopologicalSpace (LaurentSeriesPkg K).space

Equations

LaurentSeries.instTopologicalSpaceSpaceRatFuncLaurentSeriesPkg K = UniformSpace.toTopologicalSpace

source

@[simp]

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

(LaurentSeriesPkg K).coe x = ↑x

source

@[reducible, inline]

abbrev LaurentSeries.extensionAsRingHom (K : Type u_2) [Field K] (hf : Continuous ⇑(RatFunc.coeAlgHom K).toRingHom) [CompleteSpace (LaurentSeries K)] [T0Space (LaurentSeries K)] :

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

Reintrerpret the extension of coe : RatFunc K → K⸨X⸩ as ring homomorphism

Equations

LaurentSeries.extensionAsRingHom K = UniformSpace.Completion.extensionHom (RatFunc.coeAlgHom K).toRingHom

source

@[reducible, inline]

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

Type u_2

An abbreviation for the X-adic completion of RatFunc K

Equations

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

source

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

UniformSpace (RatFuncAdicCompl K)

Equations

LaurentSeries.instUniformSpaceRatFuncAdicCompl K = inferInstance

source

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

UniformSpace (LaurentSeries K)

Equations

LaurentSeries.instUniformSpace K = inferInstance

source

@[reducible, inline]

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)

source

theorem LaurentSeries.comparePkg_eq_extension (K : Type u_2) [Field K] (x : UniformSpace.Completion (RatFunc K)) :

(comparePkg K).toFun x = (↑↑(extensionAsRingHom K ⋯)).toFun x

source

@[reducible, inline]

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