Substitutions in multivariate power series #
Here we define the substitution of power series into other power series. We follow Bourbaki, Algebra II, chap. 4, §4, n° 3 who present substitution of power series as an application of evaluation.
For an R
-algebra S
, f : MvPowerSeries σ R
and a : σ → MvPowerSeries τ S
,
MvPowerSeries.subst a f
is the substitution of X s
by a s
in f
.
It is only well defined under one of the two following conditions:
f
is a polynomial, in which case it is the classical evaluation;- or the condition
MvPowerSeries.HasSubst a
holds, which means:- For every
s
, the constant coefficient ofa s
is nilpotent; - For every
d : σ →₀ ℕ
, all but finitely many of the coefficients(a s).coeff d
vanish. In the other cases, it is defined as 0 (dummy value).
- For every
When HasSubst a
, MvPowerSeries.subst a
gives rise to an algebra homomorphism
MvPowerSeries.substAlgHom ha : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S
.
We also define MvPowerSeries.rescale
which rescales a multivariate
power series f : MvPowerSeries σ R
by a map a : σ → R
and show its relation with substitution (under CommRing R
).
To stay in line with PowerSeries.rescale
, this is defined by hand
for commutative semirings.
Implementation note #
Evaluation of a power series at adequate elements has been defined
in Mathlib.RingTheory.MvPowerSeries.Evaluation
.
The goal here is to check the relevant hypotheses:
- The ring of coefficients is endowed the discrete topology.
- The main condition rewrites as having nilpotent constant coefficient
- Multivariate power series have a linear topology
The function MvPowerSeries.subst
is defined using an explicit
invocation of the discrete uniformity (⊥
).
If users need to enter the API, they can use MvPowerSeries.subst_eq_eval₂
and similar lemmas that hold for whatever uniformity on the space as soon
as it is discrete.
TODO #
MvPowerSeries.IsNilpotent_subst
asserts that the constant coefficient of a legit substitution is nilpotent; prove that the converse holds when the kernel ofalgebraMap R S
is a nilideal.
Families of power series which can be substituted
- const_coeff (s : σ) : IsNilpotent ((constantCoeff τ S) (a s))
Instances For
A multivariate power series can be substituted if and only if it can be evaluated when the topology on the coefficients ring is the discrete topology.
Families of MvPowerSeries
that can be substituted, as an Ideal
Equations
- MvPowerSeries.hasSubstIdeal = { carrier := setOf MvPowerSeries.HasSubst, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
If σ
is finite, then the nilpotent condition is enough for HasSubst
If σ
is finite, then having zero constant coefficient is enough for HasSubst
Substitution of power series into a power series
It coincides with evaluation when f
is a polynomial, or under HasSubst a
.
Otherwise, it is given the dummy value 0
.
Equations
- MvPowerSeries.subst a f = MvPowerSeries.eval₂ (algebraMap R (MvPowerSeries τ S)) a f
Instances For
For HasSubst a
, MvPowerSeries.subst
is an algebra morphism.
Equations
Instances For
Rewrite MvPowerSeries.substAlgHom
as MvPowerSeries.aeval
.
Its use is discouraged because it introduces a topology and might lead into awkward comparisons.
The ring homomorphism taking a multivariate power series f(X)
to f(aX)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rescaling a homogeneous power series
Rescale a multivariate power series, as a MonoidHom
in the scaling parameters.
Equations
- MvPowerSeries.rescaleMonoidHom = { toFun := MvPowerSeries.rescale, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Rescale a multivariate power series, as an AlgHom
in the scaling parameters,
by multiplying each variable x
by the value a x
.