Documentation

Mathlib.RingTheory.MvPowerSeries.PiTopology

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 N. Bourbaki, Algebra {II}, Chapter 4, §4, n°2.

It is not the adic topology in general.

Main results #

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

Instances #

Implementation Notes #

In Mathlib.RingTheory.MvPowerSeries.LinearTopology, we generalize the criterion for topological nilpotency by proving that, if the base ring is equipped with a linear topology, then a power series is topologically nilpotent if and only if its constant coefficient is. This is lemma MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff.

Mathematically, everything proven in this files follows from that general statement. However, formalizing this yields a few (minor) annoyances:

Since the code duplication is rather minor (the interesting part of the proof is already extracted as MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent), we just leave this as is for now. But future contributors wishing to clean this up should feel free to give it a try !

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 : ι) => (coeff R d) (f i)) u (nhds ((coeff R d) g))

A family of power series converges iff it converges coefficientwise

The semiring topology on MvPowerSeries of a topological semiring

The ring topology on MvPowerSeries of a topological ring

Scalar multiplication on MvPowerSeries is continuous.

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

See also MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff.

theorem MvPowerSeries.WithPiTopology.hasSum_of_monomials_self {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [Semiring R] (f : MvPowerSeries σ R) :
HasSum (fun (d : σ →₀ ) => (monomial R d) ((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 : σ →₀ ), (monomial R d) ((coeff R d) f)

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

Coefficients of a multivariate power series are uniformly continuous

Completeness of the uniform structure on MvPowerSeries

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

Alias of MvPowerSeries.WithPiTopology.instIsUniformAddGroup.


The IsUniformAddGroup structure on MvPowerSeries of a IsUniformAddGroup