Product topology on multivariate power series

Let R be with Semiring R and TopologicalSpace R In this file we define the topology on MvPowerSeries σ R that corresponds to the simple convergence on its coefficients. It is the coarsest topology for which all coefficient maps are continuous.

When R has UniformSpace R, we define the corresponding uniform structure.

This topology can be included by writing open scoped MvPowerSeries.WithPiTopology.

When the type of coefficients has the discrete topology, it corresponds to the topology defined by [Bou90], chapter 4, §4, n°2.

It is not the adic topology in general.

Main results

• MvPowerSeries.WithPiTopology.tendsto_pow_zero_of_constantCoeff_nilpotent, MvPowerSeries.WithPiTopology.tendsto_pow_zero_of_constantCoeff_zero: if the constant coefficient of f is nilpotent, or vanishes, then the powers of f converge to zero.

• MvPowerSeries.WithPiTopology.tendsto_pow_of_constantCoeff_nilpotent_iff : the powers of f converge to zero iff the constant coefficient of f is nilpotent.

• MvPowerSeries.WithPiTopology.hasSum_of_monomials_self : viewed as an infinite sum, a power series converges to itself.

TODO: add the similar result for the series of homogeneous components.

Instances

• If R is a topological (semi)ring, then so is MvPowerSeries σ R.
• If the topology of R is T0 or T2, then so is that of MvPowerSeries σ R.
• If R is a UniformAddGroup, then so is MvPowerSeries σ R.
• If R is complete, then so is MvPowerSeries σ R.

def MvPowerSeries.WithPiTopology.instTopologicalSpace {σ : Type u_1} (R : Type u_2) [TopologicalSpace R] : TopologicalSpace (MvPowerSeries σ R)

The pointwise topology on MvPowerSeries

Equations

• MvPowerSeries.WithPiTopology.instTopologicalSpace R = Pi.topologicalSpace

theorem MvPowerSeries.WithPiTopology.instT0Space {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [T0Space R] : T0Space (MvPowerSeries σ R)

MvPowerSeries on a T0Space form a T0Space

theorem MvPowerSeries.WithPiTopology.instT2Space {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [T2Space R] : T2Space (MvPowerSeries σ R)

MvPowerSeries on a T2Space form a T2Space

theorem MvPowerSeries.WithPiTopology.continuous_coeff {σ : Type u_1} (R : Type u_2) [TopologicalSpace R] [Semiring R] (d : σ →₀ ℕ) : Continuous ⇑(MvPowerSeries.coeff R d)

MvPowerSeries.coeff is continuous.

theorem MvPowerSeries.WithPiTopology.continuous_constantCoeff {σ : Type u_1} (R : Type u_2) [TopologicalSpace R] [Semiring R] : Continuous ⇑(MvPowerSeries.constantCoeff σ R)

MvPolynomial.constantCoeff is continuous

theorem MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [Semiring R] {ι : Type u_3} (f : ι → MvPowerSeries σ R) (u : Filter ι) (g : MvPowerSeries σ R) : Filter.Tendsto f u (nhds g) ↔ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun (i : ι) => (MvPowerSeries.coeff R d) (f i)) u (nhds ((MvPowerSeries.coeff R d) g))

A family of power series converges iff it converges coefficientwise

theorem MvPowerSeries.WithPiTopology.instTopologicalSemiring (σ : Type u_1) (R : Type u_2) [TopologicalSpace R] [Semiring R] [TopologicalSemiring R] : TopologicalSemiring (MvPowerSeries σ R)

The semiring topology on MvPowerSeries of a topological semiring

theorem MvPowerSeries.WithPiTopology.instTopologicalRing (σ : Type u_1) (R : Type u_2) [TopologicalSpace R] [Ring R] [TopologicalRing R] : TopologicalRing (MvPowerSeries σ R)

The ring topology on MvPowerSeries of a topological ring

theorem MvPowerSeries.WithPiTopology.continuous_C {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [Semiring R] : Continuous ⇑(MvPowerSeries.C σ R)

theorem MvPowerSeries.WithPiTopology.variables_tendsto_zero {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [Semiring R] : Filter.Tendsto (fun (x : σ) => MvPowerSeries.X x) Filter.cofinite (nhds 0)

theorem MvPowerSeries.WithPiTopology.tendsto_pow_zero_of_constantCoeff_nilpotent {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [CommSemiring R] {f : MvPowerSeries σ R} (hf : IsNilpotent ((MvPowerSeries.constantCoeff σ R) f)) : Filter.Tendsto (fun (n : ℕ) => f ^ n) Filter.atTop (nhds 0)

theorem MvPowerSeries.WithPiTopology.tendsto_pow_zero_of_constantCoeff_zero {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [CommSemiring R] {f : MvPowerSeries σ R} (hf : (MvPowerSeries.constantCoeff σ R) f = 0) : Filter.Tendsto (fun (n : ℕ) => f ^ n) Filter.atTop (nhds 0)

theorem MvPowerSeries.WithPiTopology.tendsto_pow_of_constantCoeff_nilpotent_iff {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [CommRing R] [DiscreteTopology R] (f : MvPowerSeries σ R) : Filter.Tendsto (fun (n : ℕ) => f ^ n) Filter.atTop (nhds 0) ↔ IsNilpotent ((MvPowerSeries.constantCoeff σ R) f)

The powers of a MvPowerSeries converge to 0 iff its constant coefficient is nilpotent. N. Bourbaki, Algebra II, [Bou90] (chap. 4, §4, n°2, corollaire de la prop. 3)

theorem MvPowerSeries.WithPiTopology.hasSum_of_monomials_self {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [Semiring R] (f : MvPowerSeries σ R) : HasSum (fun (d : σ →₀ ℕ) => (MvPowerSeries.monomial R d) ((MvPowerSeries.coeff R d) f)) f

A multivariate power series is the sum (in the sense of summable families) of its monomials

theorem MvPowerSeries.WithPiTopology.as_tsum {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [Semiring R] [T2Space R] (f : MvPowerSeries σ R) : f = ∑' (d : σ →₀ ℕ), (MvPowerSeries.monomial R d) ((MvPowerSeries.coeff R d) f)

If the coefficient space is T2, then the multivariate power series is tsum of its monomials

def MvPowerSeries.WithPiTopology.instUniformSpace {σ : Type u_1} {R : Type u_2} [UniformSpace R] : UniformSpace (MvPowerSeries σ R)

The componentwise uniformity on MvPowerSeries

Equations

• MvPowerSeries.WithPiTopology.instUniformSpace = Pi.uniformSpace fun (x : σ →₀ ℕ) => R

theorem MvPowerSeries.WithPiTopology.uniformContinuous_coeff {σ : Type u_1} (R : Type u_2) [UniformSpace R] [Semiring R] (d : σ →₀ ℕ) : UniformContinuous fun (f : MvPowerSeries σ R) => (MvPowerSeries.coeff R d) f

Coefficients of a multivariate power series are uniformly continuous

theorem MvPowerSeries.WithPiTopology.instCompleteSpace {σ : Type u_1} {R : Type u_2} [UniformSpace R] [CompleteSpace R] : CompleteSpace (MvPowerSeries σ R)

Completeness of the uniform structure on MvPowerSeries

theorem MvPowerSeries.WithPiTopology.instUniformAddGroup {σ : Type u_1} {R : Type u_2} [UniformSpace R] [AddGroup R] [UniformAddGroup R] : UniformAddGroup (MvPowerSeries σ R)

The UniformAddGroup structure on MvPowerSeries of a UniformAddGroup