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

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

• MvPowerSeries.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.

• 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 IsUniformAddGroup, then so is MvPowerSeries σ R.
• If R is complete, then so is MvPowerSeries σ R.

Implementation Notes

In Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean, 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:

• we would need to push the results in this file slightly lower in the import tree (likely, in a new dedicated file);
• we would have to work in CommRings rather than CommSemirings (this probably does not matter in any way though);
• because isTopologicallyNilpotent_of_constantCoeff_isNilpotent holds for any topology, not necessarily discrete nor linear, the proof going through the general case involves juggling a bit with the topologies.

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 !

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.instTopologicalSpace_mono (σ : Type u_3) {R : Type u_4} {t u : TopologicalSpace R} (htu : t ≤ u) : instTopologicalSpace R ≤ instTopologicalSpace R

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 ⇑(coeff R d)

MvPowerSeries.coeff is continuous.

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

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

A family of power series converges iff it converges coefficientwise

theorem MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [DecidableEq σ] [CommSemiring R] (f : MvPowerSeries σ R) : Filter.Tendsto (fun (d : σ →₀ ℕ) => ↑((trunc' R d) f)) Filter.atTop (nhds f)

theorem MvPowerSeries.WithPiTopology.tendsto_trunc_atTop {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [DecidableEq σ] [CommSemiring R] [Nonempty σ] (f : MvPowerSeries σ R) : Filter.Tendsto (fun (d : σ →₀ ℕ) => ↑((trunc R d) f)) Filter.atTop (nhds f)

theorem MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [CommSemiring R] : DenseRange MvPolynomial.toMvPowerSeries

The inclusion of polynomials into power series has dense image

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

The semiring topology on MvPowerSeries of a topological semiring

theorem MvPowerSeries.WithPiTopology.instIsTopologicalRing (σ : Type u_1) (R : Type u_2) [TopologicalSpace R] [Ring R] [IsTopologicalRing R] : IsTopologicalRing (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 ⇑(C σ R)

instance MvPowerSeries.WithPiTopology.instContinuousSMul {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] {S : Type u_3} [Semiring S] [TopologicalSpace S] [CommSemiring R] [Algebra R S] [ContinuousSMul R S] : ContinuousSMul R (MvPowerSeries σ S)

Scalar multiplication on MvPowerSeries is continuous.

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

theorem MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [CommSemiring R] {f : MvPowerSeries σ R} (hf : IsNilpotent ((constantCoeff σ R) f)) : IsTopologicallyNilpotent f

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

theorem MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent {σ : Type u_1} {R : Type u_2} [TopologicalSpace R] [CommRing R] [DiscreteTopology R] (f : MvPowerSeries σ R) : IsTopologicallyNilpotent f ↔ IsNilpotent ((constantCoeff σ R) f)

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

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) => (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.instIsUniformAddGroup {σ : Type u_1} {R : Type u_2} [UniformSpace R] [AddGroup R] [IsUniformAddGroup R] : IsUniformAddGroup (MvPowerSeries σ R)

The IsUniformAddGroup structure on MvPowerSeries of a IsUniformAddGroup

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

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

Alias of MvPowerSeries.WithPiTopology.instIsUniformAddGroup.

---

The IsUniformAddGroup structure on MvPowerSeries of a IsUniformAddGroup