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 off
is nilpotent, or vanishes, thenf
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 off
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 isMvPowerSeries σ R
. - If the topology of
R
is T0 or T2, then so is that ofMvPowerSeries σ R
. - If
R
is aIsUniformAddGroup
, then so isMvPowerSeries σ R
. - If
R
is complete, then so isMvPowerSeries σ R
.
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:
- 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
CommRing
s rather thanCommSemiring
s (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 !
The pointwise topology on MvPowerSeries
Instances For
MvPowerSeries
on a T0Space
form a T0Space
MvPowerSeries
on a T2Space
form a T2Space
MvPowerSeries.coeff
is continuous.
MvPowerSeries.constantCoeff
is continuous
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
.
A multivariate power series is the sum (in the sense of summable families) of its monomials
The componentwise uniformity on MvPowerSeries
Equations
- MvPowerSeries.WithPiTopology.instUniformSpace = Pi.uniformSpace fun (x : σ →₀ ℕ) => R
Instances For
Coefficients of a multivariate power series are uniformly continuous
Completeness of the uniform structure on MvPowerSeries
The IsUniformAddGroup
structure on MvPowerSeries
of a IsUniformAddGroup
Alias of MvPowerSeries.WithPiTopology.instIsUniformAddGroup
.
The IsUniformAddGroup
structure on MvPowerSeries
of a IsUniformAddGroup