Product topology on power series

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

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

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

When the type of coefficients has the discrete topology, it corresponds to the topology defined by N. Bourbaki, Algebra {II}, Chapter 4, §4, n°2.

It corresponds with the adic topology but this is not proved here.

• PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero: if the constant coefficient of f is nilpotent, or vanishes, then f is topologically nilpotent.

• PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent : assuming the base ring has the discrete topology, f is topologically nilpotent iff the constant coefficient of f is nilpotent.

• PowerSeries.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 PowerSeries σ R.
• If the topology of R is T0 or T2, then so is that of PowerSeries σ R.
• If R is a IsUniformAddGroup, then so is PowerSeries σ R.
• If R is complete, then so is PowerSeries σ R.

def PowerSeries.WithPiTopology.instTopologicalSpace (R : Type u_1) [TopologicalSpace R] : TopologicalSpace (PowerSeries R)

The pointwise topology on PowerSeries

Equations

• PowerSeries.WithPiTopology.instTopologicalSpace R = Pi.topologicalSpace

theorem PowerSeries.WithPiTopology.instT0Space (R : Type u_1) [TopologicalSpace R] [T0Space R] : T0Space (PowerSeries R)

Separation of the topology on PowerSeries

theorem PowerSeries.WithPiTopology.instT2Space (R : Type u_1) [TopologicalSpace R] [T2Space R] : T2Space (PowerSeries R)

PowerSeries on a T2Space form a T2Space

theorem PowerSeries.WithPiTopology.continuous_coeff (R : Type u_1) [TopologicalSpace R] [Semiring R] (d : ℕ) : Continuous ⇑(coeff d)

Coefficients are continuous

theorem PowerSeries.WithPiTopology.continuous_constantCoeff (R : Type u_1) [TopologicalSpace R] [Semiring R] : Continuous ⇑constantCoeff

The constant coefficient is continuous

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

A family of power series converges iff it converges coefficientwise

theorem PowerSeries.WithPiTopology.tendsto_trunc_atTop (R : Type u_1) [TopologicalSpace R] [CommSemiring R] (f : PowerSeries R) : Filter.Tendsto (fun (d : ℕ) => ↑(trunc d f)) Filter.atTop (nhds f)

theorem PowerSeries.WithPiTopology.denseRange_toPowerSeries (R : Type u_1) [TopologicalSpace R] [CommSemiring R] : DenseRange Polynomial.toPowerSeries

The inclusion of polynomials into power series has dense image

theorem PowerSeries.WithPiTopology.instIsTopologicalSemiring (R : Type u_1) [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] : IsTopologicalSemiring (PowerSeries R)

The semiring topology on PowerSeries of a topological semiring

theorem PowerSeries.WithPiTopology.instIsTopologicalRing (R : Type u_1) [TopologicalSpace R] [Ring R] [IsTopologicalRing R] : IsTopologicalRing (PowerSeries R)

The ring topology on PowerSeries of a topological ring

theorem PowerSeries.WithPiTopology.hasSum_iff_hasSum_coeff (R : Type u_1) [TopologicalSpace R] [Semiring R] {ι : Type u_2} {f : ι → PowerSeries R} {g : PowerSeries R} : HasSum f g ↔ ∀ (d : ℕ), HasSum (fun (i : ι) => (coeff d) (f i)) ((coeff d) g)

theorem PowerSeries.WithPiTopology.summable_iff_summable_coeff (R : Type u_1) [TopologicalSpace R] [Semiring R] {ι : Type u_2} {f : ι → PowerSeries R} : Summable f ↔ ∀ (d : ℕ), Summable fun (i : ι) => (coeff d) (f i)

theorem PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top (R : Type u_1) [TopologicalSpace R] [Semiring R] {ι : Type u_2} {f : ι → PowerSeries R} [LinearOrder ι] [LocallyFiniteOrderBot ι] (h : Filter.Tendsto (fun (i : ι) => (f i).order) Filter.atTop (nhds ⊤)) : Summable f

A family of PowerSeries is summable if their order tends to infinity.

def PowerSeries.WithPiTopology.instUniformSpace (R : Type u_1) [UniformSpace R] : UniformSpace (PowerSeries R)

The product uniformity on PowerSeries

Equations

• PowerSeries.WithPiTopology.instUniformSpace R = MvPowerSeries.WithPiTopology.instUniformSpace

theorem PowerSeries.WithPiTopology.uniformContinuous_coeff (R : Type u_1) [UniformSpace R] [Semiring R] (d : ℕ) : UniformContinuous fun (f : PowerSeries R) => (coeff d) f

Coefficients are uniformly continuous

theorem PowerSeries.WithPiTopology.instCompleteSpace (R : Type u_1) [UniformSpace R] [CompleteSpace R] : CompleteSpace (PowerSeries R)

Completeness of the uniform structure on PowerSeries

theorem PowerSeries.WithPiTopology.instIsUniformAddGroup (R : Type u_1) [UniformSpace R] [AddGroup R] [IsUniformAddGroup R] : IsUniformAddGroup (PowerSeries R)

The IsUniformAddGroup structure on PowerSeries of a IsUniformAddGroup

@[deprecated PowerSeries.WithPiTopology.instIsUniformAddGroup (since := "2025-03-27")]

theorem PowerSeries.WithPiTopology.instUniformAddGroup (R : Type u_1) [UniformSpace R] [AddGroup R] [IsUniformAddGroup R] : IsUniformAddGroup (PowerSeries R)

Alias of PowerSeries.WithPiTopology.instIsUniformAddGroup.

---

The IsUniformAddGroup structure on PowerSeries of a IsUniformAddGroup

theorem PowerSeries.WithPiTopology.continuous_C {R : Type u_1} [TopologicalSpace R] [Semiring R] : Continuous ⇑C

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

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

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

Assuming the base ring has a discrete topology, the powers of a PowerSeries converge to 0 iff its constant coefficient is nilpotent. N. Bourbaki, Algebra {II}, Chapter 4, §4, n°2, corollary of prop. 3

theorem PowerSeries.hasSum_of_monomials_self {R : Type u_1} [Semiring R] [TopologicalSpace R] (f : PowerSeries R) : HasSum (fun (d : ℕ) => (monomial d) ((coeff d) f)) f

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

theorem PowerSeries.as_tsum {R : Type u_1} [Semiring R] [TopologicalSpace R] [T2Space R] (f : PowerSeries R) : f = ∑' (d : ℕ), (monomial d) ((coeff d) f)

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