Restricted Power Series #
This file defines restricted power series A⟨T₁, …, Tₖ⟩, following Wedhorn's Adic Spaces,
where the convergent/restricted power series ring is (5.6.1) in §5.6.
Main definitions #
IsRestricted: A power series is restricted if its coefficients converge to0along the cofinite filter on multi-indices. The coefficients are asked only for a0and a topology, so the same predicate serves ring and module coefficients.restrictedMvPowerSeriesSubring k A: The subring of restricted power series inkvariables overA, denotedA⟨T₁, …, Tₖ⟩.restrictedMvPowerSeriesSubmodule k A M: theA-submodule of restricted power series with coefficients in a topologicalA-moduleM, denotedM⟨T₁, …, Tₖ⟩. This is the object Wedhorn's Remark 8.29 compares withM ⊗[A] A⟨T₁, …, Tₖ⟩. It is Mathlib'sFilter.zeroAtFilterSubmoduleat the cofinite filter, under the Huber-theoretic name.restrictedMvPowerSeriesSubringVal: the inclusionA⟨T₁, …, Tₖ⟩ → MvPowerSeries (Fin k) Aas anA-algebra map.A⟨T⟩is aSubringcarrying anAlgebra Ainstance rather than aSubalgebra, soSubalgebra.valdoes not apply.isRestricted_of_hasFiniteSupport: the introduction rule at module coefficients — finitely many nonzero coefficients suffice.isRestricted_pi_iff: restrictedness of a series with coefficients in a product is componentwise.restrictedMvPowerSeriesSubringLinearEquiv: atM = Athe subring and the submodule of restricted series areA-linearly isomorphic.restrictedMvPowerSeriesSubmoduleMap:M ↦ M⟨T₁, …, Tₖ⟩is functorial in zero-continuousA-linear maps, withIsRestricted.mapat the predicate level and the two functor laws.restrictedMvPowerSeriesSubmoduleMap_surjective: that functor preserves open surjections out of a module with a countable neighbourhood basis at0— the lifted coefficients can then be chosen to still tend to0, which lifting them one at a time does not give. This is what lets Wedhorn's Remark 8.29 descend from a presentation.restrictedMvPowerSeriesSubmoduleMap_eq_zero_iffandrestrictedMvPowerSeriesSubmoduleMap_injective: the kernel of the induced map is detected coefficientwise, so the functor preserves injectivity. Together withrestrictedMvPowerSeriesSubmoduleMap_surjectivethese are the exactness inputs Remark 8.29 needs at the two ends.restrictedMvPowerSeriesSubmoduleMap_range_eq_ker: and the input it needs in the middle — forrange u = ker pwithuopen onto its image, the induced row is exact atN⟨T₁, …, Tₖ⟩. With the two above, Remark 8.29's row is exact everywhere.restrictedMvPowerSeriesSubmodule_ext: coefficientwise agreement is equality inM⟨T₁, …, Tₖ⟩— the elimination ruleMvPowerSeries.extcannot supply at module coefficients.coeff_coe_smul_restrictedMvPowerSeriesSubring: the scalar action onA⟨T₁, …, Tₖ⟩is coefficientwise multiplication — the subring's action isAlgebra.smul_def, not pointwise.restrictedMvPowerSeriesSubmodulePiEquiv: that criterion as anA-linear equivalence,(∏ i, M i)⟨T₁, …, Tₖ⟩ ≃ₗ[A] ∏ i, M i⟨T₁, …, Tₖ⟩.
Provenance #
This module is a port of AINTLIB's projects/AdicSpaces/Adic spaces/RestrictedPowerSeries.lean,
the roadmap's designated prior formalisation of this material. Three groups, because the port and
this PR did different things to different declarations.
AINTLIB's in definition, statement and proof. restrictedMvPowerSeriesSubring,
restrictedMvPowerSeriesSubring.instAlgebra, IsRestricted.finite_coeff_notMem, the private
helpers finite_shift_bad_set and coeff_mul_mem_of_forall_mem, and IsRestricted.mul — the
convolution argument this file exists for. That convolution argument is AINTLIB's; what differs
here is three call sites renamed to isRestricted_iff_coeff, and the choice of absorbing
neighbourhood, which now comes from Mathlib's exists_mem_nhds_zero_mul_subset on the left and
TauCeti.Huber.isBounded_finite on the right, in place of AINTLIB's inline Aᵐᵒᵖ transport.
AINTLIB's in statement, with proofs rewritten here. Five: isRestricted_zero,
IsRestricted.add and IsRestricted.neg, which now delegate to Mathlib's Filter.ZeroAtFilter
API instead of reproving convergence; and isRestricted_one and isRestricted_algebraMap, which
were near-identical tendsto_nhds/mem_cofinite arguments and are now special cases of
isRestricted_of_hasFiniteSupport. IsRestricted itself is AINTLIB's statement at weaker
coefficient binders — [Zero] and a topology, where the original asked for a semiring.
Original here. isRestricted_monomial, isRestricted_of_hasFiniteSupport,
IsRestricted.smul, restrictedMvPowerSeriesSubmodule, mem_restrictedMvPowerSeriesSubmodule,
isRestricted_pi_iff, restrictedMvPowerSeriesSubmodulePiEquiv and
restrictedMvPowerSeriesSubringLinearEquiv, each with its computation lemmas, together with
IsRestricted.map, restrictedMvPowerSeriesSubmoduleMap with its laws,
restrictedMvPowerSeriesSubmoduleMap_surjective,
restrictedMvPowerSeriesSubmoduleMap_eq_zero_iff and
restrictedMvPowerSeriesSubmoduleMap_injective, and
coeff_coe_smul_restrictedMvPowerSeriesSubring.
None of those has an AINTLIB counterpart, for three different reasons.
restrictedMvPowerSeriesSubmoduleMap_surjective has none for the same reason as the rest of the
induced-map material: AINTLIB states restricted series over a coefficient ring only, so it has no
induced map at module coefficients and a fortiori no surjectivity statement about one. Wedhorn
Remark 8.29 is credited for the mathematics; the lifting construction it delegates to
(TauCeti.exists_lift_tendsto_cofinite_nhds) is original here too.
restrictedMvPowerSeriesSubmoduleMap_eq_zero_iff and
restrictedMvPowerSeriesSubmoduleMap_injective are the same statement at the other end of the
exactness, and have no counterpart there for the same reason.
The two product statements — isRestricted_pi_iff and restrictedMvPowerSeriesSubmodulePiEquiv —
have none because the source states restrictedness only for a single coefficient module and never
for a product, so neither the criterion nor the equivalence packaging it appears there. Of those
two, isRestricted_pi_iff's content is Mathlib's tendsto_pi_nhds, so what is original in it is
the statement rather than the argument, while the equivalence is original in both.
IsRestricted.map, restrictedMvPowerSeriesSubmoduleMap and its laws have none because the
source states restricted series only over a coefficient ring: there is no module argument there
to be functorial in, so no map to credit. The general filter content of IsRestricted.map is
Filter.ZeroAtFilter.comp, which this repo supplies.
restrictedMvPowerSeriesSubringLinearEquiv has none because the source never introduces the
submodule at all, so the subring is the only object it has to identify. The same holds of
coeff_coe_smul_restrictedMvPowerSeriesSubring, which computes an action the source never
states.
AINTLIB's mathematics, generalised in statement and rebuilt on this file's API.
restrictedMvPowerSeriesSubmoduleMap_range_eq_ker is AINTLIB's muMap_middle_exact
(Adic spaces/TateAlgebra.lean:1855), Wedhorn's own middle-exactness step, and the argument is
that one: corestrict u to its image, lift the coefficients of a series killed by p along the
corestriction, compose back. Three things differ. The source fixes the row to Aⁿ → Aᵐ → M and
carries Wedhorn's bundle — [CompleteSpace A] [IsTateRing A] [IsNoetherianRing A] — so as to
derive strictness of u from its own wedhorn_6_18_open_onto_image; the row here is between
arbitrary topological modules with strictness hypothesised, so none of that bundle appears. The
source works at ring coefficients through its own restrictedModule and lifts with
restrictedModule_map_surjective; both come from this file's module-coefficient functor here.
And the continuity of the action on ↥(range u), which the source establishes inline, is
Submodule.continuousConstSMul.
The name isRestricted_iff needs care: the port introduced it for the coeff-form unfolding
lemma, which is now isRestricted_iff_coeff. The statement the name carries here — unfolding
through Filter.ZeroAtFilter at coefficients asking only for a 0 and a topology — is new.
That originality claim was checked against both AINTLIB sources the roadmap designates for
this material, not only RestrictedPowerSeries.lean. AINTLIB's TateAlgebra.lean,
TateAlgebraTopology.lean and TateAlgebraWedhorn.lean build TateAlgebra A for a ring A
([CommRing A] [TopologicalSpace A] [NonarchimedeanRing A]) throughout; their Submodule
occurrences are ideals of that ring viewed as submodules, not coefficients in a module. There is
no M⟨X⟩ there, and §0.5's "restricted series with coefficients in a complete topological module"
has no AINTLIB counterpart to credit.
The port additionally moves the declarations into the TauCeti.Huber namespace, opts into the
Lean module system with the definition bodies unexposed — hence the added isRestricted_iff_coeff,
mem_restrictedMvPowerSeriesSubring and coe_algebraMap_restrictedMvPowerSeriesSubring — tracks
the Mathlib rename of Set.mem_setOf_eq to
Set.mem_ofPred_eq, renames the predicate from AINTLIB's IsRestrictedAdic (nothing here is
adic), and drops hypotheses that the individual proofs never used.
This is not Mathlib's MvPowerSeries.IsRestricted, which is stated over a normed ring and
relative to a polyradius c : σ → ℝ, asking that ‖coeff t f‖ * ∏ i, c i ^ t i tend to 0 along
the cofinite filter. The two conditions agree over a normed ring at c = 1, but neither is more
general: Mathlib's varies the radius, while IsRestricted here needs no norm — indeed no
multiplication, asking the coefficients for nothing beyond a 0 and a topology. It is the
norm-free form that Huber theory requires: Huber ring topologies are defined using an ideal of
definition and need not be induced by a norm. The nonarchimedean hypothesis enters only for
closure under multiplication, and hence for the subring but not for the submodule.
Implementation notes #
The restricted power series ring is defined as a subring of MvPowerSeries (Fin k) A
(the formal power series ring), cut out by the condition that coefficients tend to 0.
This is the canonical concrete definition. M⟨T₁, …, Tₖ⟩ is cut out of
MvPowerSeries (Fin k) M by the same condition, as an A-submodule.
IsRestricted is Mathlib's Filter.ZeroAtFilter at the cofinite filter, applied to the
coefficient function — see isRestricted_iff, which is Iff.rfl. The closure
lemmas delegate to zero_zeroAtFilter and ZeroAtFilter.add/.neg/.smul, and
restrictedMvPowerSeriesSubmodule is Filter.zeroAtFilterSubmodule at that filter rather than
a reconstruction of it. The Huber-specific names are kept because M⟨T₁, …, Tₖ⟩ is the object the
roadmap names, but no closure property is proved here that Mathlib already has.
isRestricted_iff unfolds the predicate through Filter.ZeroAtFilter, which is the form the
delegations use and what module coefficients admit; isRestricted_iff_coeff unfolds it through
MvPowerSeries.coeff, the accessor to prefer wherever the coefficients form a semiring. The two
agree definitionally, because coeff is projection.
isRestricted_of_hasFiniteSupport delegates separately, through tendsto_cofinite_pure_iff, and
isRestricted_one and isRestricted_algebraMap are its special cases at 1 and at a constant.
The closure of the restricted power series under multiplication (convolution) requires
that A is a topological ring. The proof that the convolution of two sequences tending
to 0 also tends to 0 uses the nonarchimedean property to ensure that
arbitrary finite sums of elements in an open additive subgroup remain in the subgroup.
References #
- Wedhorn, Adic Spaces, (5.6.1) in §5.6, and Remark 8.29.
- AINTLIB, branch
dev/adic-spaces,projects/AdicSpaces/Adic spaces/RestrictedPowerSeries.leanand, at commit37bbdaeb9,projects/AdicSpaces/Adic spaces/TateAlgebra.lean.
Restricted power series #
An element f of the multivariate power series ring M⦃X₁, …, Xₖ⦄ is restricted
if its coefficients converge to 0 along the cofinite filter on multi-indices. That is,
for every open neighborhood U of 0 in M, all but finitely many coefficients of f
lie in U. This is the defining property of elements of M⟨T₁, …, Tₖ⟩, and of
A⟨T₁, …, Tₖ⟩ in the case of ring coefficients.
The coefficients need carry no algebraic structure beyond a distinguished 0: the condition is
about a family of points converging in M. Stronger binders appear below wherever the statement
names an operation, because that is where Mathlib's MvPowerSeries instances put the floor —
f + g needs [AddMonoid M] and c • f needs [Module R M] for the expression to be
well-formed at all, not because the convergence argument needs them. The module coefficients used
for M⟨X⟩ are not a semiring, which is why the predicate itself must not ask for one.
See Wedhorn, (5.6.1) and §6.7.
Equations
- TauCeti.Huber.IsRestricted f = Filter.Tendsto (fun (s : Fin k →₀ ℕ) => f s) Filter.cofinite (nhds 0)
Instances For
IsRestricted is Filter.ZeroAtFilter at the cofinite filter, on the coefficient
function. Mathlib's predicate is the general notion — a function tending to 0 along a filter —
and restrictedness is its instance at cofinite. The body is not exposed, so this is how a
consumer at module coefficients recovers the defining condition.
Unfolding lemma for TauCeti.Huber.IsRestricted over a semiring, through
MvPowerSeries.coeff. The body is not exposed, so this is how consumers recover the defining
convergence condition where the coefficients form a semiring.
A series with coefficients in a product is restricted exactly when each of its components
is. No finiteness of ι is needed: the product topology is the topology of pointwise convergence,
so the criterion holds for an arbitrary product.
The two sides are equivalent, not identical — unlike isRestricted_iff_coeff and
mem_restrictedMvPowerSeriesSubmodule, whose (Iff.rfl) proofs mark a genuine defeq, this one
is not a definitional unfolding.
Deliberately not @[simp]: the right-hand side is a componentwise form that no other lemma in
this file can act on, so tagging it would rewrite IsRestricted goals at product coefficients into
a dead end for anything beyond the lemmas that already close them.
0 is restricted: its coefficients are constantly 0.
A series with finite support is restricted.
A sufficient condition, and the convenient introduction rule at module coefficients, where the
closure lemmas only combine existing members. isRestricted_monomial is its case at a single
index, and isRestricted_one and isRestricted_algebraMap follow from that.
A monomial is restricted: its support is contained in {n}, and is empty when a = 0.
The constant series are the case n = 0: isRestricted_one and isRestricted_algebraMap follow
from monomial 0 1 and monomial 0 a. Unlike isRestricted_algebraMap this needs no
commutativity, so it also covers C a over a noncommutative semiring.
1 is restricted: every coefficient but the 0-th vanishes.
A sum of restricted series is restricted.
The negation of a restricted series is restricted.
Scaling a restricted series by a constant leaves it restricted.
R need not be the coefficients' own ring: any semiring acting on M will do, and what the
scaling asks beyond that module structure is continuity of each c • · in the vector variable,
which is ContinuousConstSMul. Stated so that consumers holding IsRestricted can use it
directly, as they can IsRestricted.add and IsRestricted.neg.
A zero-preserving map that is continuous at 0 pushes restricted series forward: φ ∘ f
is restricted whenever f is. Restrictedness is convergence of the coefficients to 0 along
cofinite, so only the behaviour of φ at 0 is involved; global continuity is not needed.
restrictedMvPowerSeriesSubmoduleMap takes the same hypothesis, and not the stronger one, because
they do not coincide here: continuity at 0 upgrades to global continuity for a linear map
only when the topology is translation-invariant, and these modules carry ContinuousAdd rather
than IsTopologicalAddGroup. A caller holding Continuous φ passes hφ.continuousAt.
The show fixes the elaboration of the coefficient function as a MvPowerSeries: that type is a
plain def for (Fin k →₀ ℕ) → N, so without the ascription the lambda elaborates at the bare
function type and IsRestricted does not apply to it.
Restrictedness, restated: for every open additive subgroup W, all but finitely many
coefficients lie in W. This is the form the convolution argument actually consumes.
A product of restricted series is restricted. This is the only field of
restrictedMvPowerSeriesSubring that needs A nonarchimedean: the coefficient convolution is
a finite sum, and it is nonarchimedeanness that keeps such a sum inside an open subgroup.
The set of restricted power series forms a subring of MvPowerSeries (Fin k) A.
The closure under multiplication (convolution of tendsto-0 coefficient sequences)
requires that A is a nonarchimedean topological ring (so that finite sums of elements in an
open additive subgroup remain in the subgroup). This is the canonical definition of
A⟨T₁, …, Tₖ⟩ (Wedhorn, (5.6.1)/§5.6).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in A⟨T₁, …, Tₖ⟩ is restrictedness.
The variable Xᵢ of A⟨X₁, …, Xₖ⟩, as an element of the restricted subring.
Equations
Instances For
restrictedX i is the power series Xᵢ underneath.
Algebra instance #
Constant power series are restricted: the algebraMap image of any a : A has
coefficient a at multi-index 0 and 0 elsewhere, so it trivially tends to 0.
The restricted power series subring inherits an A-algebra structure from the
MvPowerSeries algebra instance, since constant power series are restricted.
Equations
- One or more equations did not get rendered due to their size.
The algebra structure on A⟨T₁, …, Tₖ⟩ is the one inherited from MvPowerSeries: a constant
is sent to the constant power series. This characterises the instance, whose body is not
exposed.
The inclusion A⟨T₁, …, Tₖ⟩ → MvPowerSeries (Fin k) A as an A-algebra map. A⟨T⟩ is a
Subring carrying an Algebra A instance rather than a Subalgebra, so Subalgebra.val does
not apply.
Equations
- TauCeti.Huber.restrictedMvPowerSeriesSubringVal = { toRingHom := (TauCeti.Huber.restrictedMvPowerSeriesSubring k A).subtype, commutes' := ⋯ }
Instances For
restrictedMvPowerSeriesSubringVal is the underlying series. Its body is not exposed, so this
is how a consumer computes with it.
Module coefficients #
M⟨T₁, …, Tₖ⟩: the restricted power series with coefficients in a topological A-module M,
as an A-submodule of M⦃T₁, …, Tₖ⦄.
This is the module-coefficient counterpart of restrictedMvPowerSeriesSubring, and it is what
Wedhorn's Remark 8.29 compares with M ⊗[A] A⟨T₁, …, Tₖ⟩. No multiplication is involved, so M
needs no ring structure and the nonarchimedean hypothesis that restrictedMvPowerSeriesSubring
carries is absent here: closure under the scalar action follows from continuity of each
a • · alone.
Equations
Instances For
Membership in M⟨T₁, …, Tₖ⟩ is restrictedness.
Coefficientwise extensionality for M⟨T₁, …, Tₖ⟩. Mathlib's MvPowerSeries.ext is stated
in a Semiring section, so it does not apply at module coefficients; without this a consumer has
to reach for Subtype.ext (funext …) and cross the MvPowerSeries-is-a-def gap by hand.
M ↦ M⟨T₁, …, Tₖ⟩ is functorial: an A-linear map continuous at 0 induces one on
restricted series, coefficientwise. Only continuity at 0 is used — see IsRestricted.map.
Equations
Instances For
restrictedMvPowerSeriesSubmoduleMap is φ coefficientwise. Its body is not exposed, so this
is how a consumer computes with it.
The identity induces the identity.
The induced maps compose.
A strict surjection stays surjective on restricted series. If φ is a surjective
A-linear map which is continuous at 0 and carries the neighbourhoods of 0 onto
neighbourhoods of 0, and M has a countable neighbourhood basis at 0, then every restricted
series with coefficients in N is the image of one with coefficients in M.
Countability of 𝓝 (0 : M) is what supplies the antitone basis the lifted coefficients are drawn
from, so it is a genuine restriction on M and not bookkeeping.
Surjectivity coefficientwise is immediate from surjectivity of φ; what is not, and what openness
supplies, is that the chosen preimages can be made to converge. Lifting each coefficient
independently can leave the lifts spread out even though the original coefficients tend to 0, in
which case the lift is a power series but not a restricted one. See
TauCeti.exists_lift_tendsto_cofinite_nhds, where the choice is made.
This is the step Wedhorn's Remark 8.29 needs in order to descend from a presentation: applied to a
presentation Aᵐ ↠ M, together with the finite free case, it is what makes the comparison map for
a finitely generated M surjective.
The hypothesis is the filter inequality the proof actually consumes rather than IsOpenMap φ,
which is strictly stronger here: these modules carry ContinuousAdd rather than
IsTopologicalAddGroup, so without translation invariance global openness does not follow from
openness at 0. A caller holding IsOpenMap φ — over a Tate ring, from
TauCeti.Huber.IsTateRing.isOpenMap — passes map_zero φ ▸ hopen.nhds_le 0.
The kernel is coefficientwise: a restricted series is killed by φ exactly when every
one of its coefficients is.
Stated as … = 0 rather than as membership in LinearMap.ker, because LinearMap.mem_ker is
itself a simp lemma: it rewrites the membership away first, so a mem_ker phrasing could not
be @[simp] — the two chain together, and f ∈ ker … still reduces coefficientwise.
M ↦ M⟨T₁, …, Tₖ⟩ preserves injectivity.
M ↦ M⟨T₁, …, Tₖ⟩ is exact in the middle. For A-linear maps u : M →ₗ[A] N and
p : N →ₗ[A] P, each continuous at 0, with range u = ker p, the induced row
M⟨T₁, …, Tₖ⟩ → N⟨T₁, …, Tₖ⟩ → P⟨T₁, …, Tₖ⟩ is exact at the middle — provided u is strict,
carrying the neighbourhoods of 0 onto neighbourhoods of 0 in its image, and M has a
countable neighbourhood basis at 0.
This is the middle-exactness step of Wedhorn's Remark 8.29: applied to a presentation
Aⁿ →u Aᵐ →p M → 0 it makes the restricted-series row exact at Aᵐ⟨T₁, …, Tₖ⟩, which is the
input the injective half of that remark runs a diagram chase against.
restrictedMvPowerSeriesSubmoduleMap_injective and
restrictedMvPowerSeriesSubmoduleMap_surjective are the same statement at the two ends.
Strictness does not follow from continuity and is not derived here. It is Wedhorn's
Proposition 6.18(2) that supplies it in the setting Remark 8.29 is stated in — over a complete
noetherian Tate ring a linear map of finitely generated modules is open onto its image — and that
derivation needs hypotheses this file does not carry. So strictness is taken as a hypothesis, in
the filter-inequality form restrictedMvPowerSeriesSubmoduleMap_surjective also takes it: a
caller holding h : IsOpenMap u.rangeRestrict passes map_zero _ ▸ h.nhds_le 0.
Only u need be strict. Nothing is asked of p beyond continuity at 0, and nothing at all of
N or P beyond what N⟨T₁, …, Tₖ⟩ and P⟨T₁, …, Tₖ⟩ need to exist: exactness at the middle
lifts the coefficients of a series killed by p along u, and the countable basis that lifting
consumes is a property of the source.
Stated as the equality of submodules rather than through Mathlib's Function.Exact, whose file
this one does not import; LinearMap.exact_iff converts in either direction where it is wanted.
A⟨T₁, …, Tₖ⟩ as a submodule over itself: at M = A the subring and the submodule cut
out the same series, so they are A-linearly isomorphic.
They are different structures over one carrier — restrictedMvPowerSeriesSubring is a Subring
carrying an Algebra A instance, restrictedMvPowerSeriesSubmodule is a Submodule A — so the
identification is not a coercion. It is what lets a statement about M⟨T⟩ at M = A meet the
tensor-product API, which produces the subring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
restrictedMvPowerSeriesSubringLinearEquiv is the identity on the underlying series. Its body
is not exposed, so this is how a consumer computes with it.
The scalar action on A⟨T₁, …, Tₖ⟩ is coefficientwise multiplication.
The subring carries an Algebra A instance, so a • f is algebraMap a * f rather than a
pointwise action; this is the lemma that gets a consumer from one to the other.
Its inverse is likewise the identity on the underlying series.
(∏ i, M i)⟨T₁, …, Tₖ⟩ is ∏ i, M i⟨T₁, …, Tₖ⟩: a restricted series valued in a product
is the tuple of its componentwise restricted series, A-linearly.
No finiteness of the index is needed. This is the target half of Wedhorn's Remark 8.29 in the
finite free case, where M is Fin n → A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
restrictedMvPowerSeriesSubmodulePiEquiv reads off the i-th component. Its body is not
exposed, so this is how a consumer computes with it.
The inverse of restrictedMvPowerSeriesSubmodulePiEquiv assembles a tuple of restricted
series into one.