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][bourbaki1981] 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:
fis a polynomial, in which case it is the classical evaluation;- or the condition
MvPowerSeries.HasSubst aholds, which means:- For every
s, the constant coefficient ofa sis nilpotent; - For every
d : σ →₀ ℕ, all but finitely many of the coefficients(a s).coeff dvanish. 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.lean.
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_substasserts that the constant coefficient of a legit substitution is nilpotent; prove that the converse holds when the kernel ofalgebraMap R Sis a nilideal.
structure
MvPowerSeries.HasSubst
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
(a : σ → MvPowerSeries τ S)
:
Families of power series which can be substituted
- const_coeff (s : σ) : IsNilpotent ((constantCoeff τ S) (a s))
theorem
MvPowerSeries.coeff_zero_iff
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
{a : σ → MvPowerSeries τ S}
[TopologicalSpace S]
[DiscreteTopology S]
:
theorem
MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
{a : σ → MvPowerSeries τ S}
[TopologicalSpace S]
[DiscreteTopology S]
:
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.
theorem
MvPowerSeries.HasSubst.hasEval
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
{a : σ → MvPowerSeries τ S}
[TopologicalSpace S]
(ha : HasSubst a)
:
HasEval a
theorem
MvPowerSeries.HasSubst.mul_left
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
(b : σ → MvPowerSeries τ S)
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
:
theorem
MvPowerSeries.HasSubst.mul_right
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
(b : σ → MvPowerSeries τ S)
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
:
theorem
MvPowerSeries.HasSubst.smul
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
(r : MvPowerSeries τ S)
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
:
noncomputable def
MvPowerSeries.hasSubstIdeal
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
:
Ideal (σ → MvPowerSeries τ S)
Families of MvPowerSeries that can be substituted, as an Ideal
Equations
- MvPowerSeries.hasSubstIdeal = { carrier := setOf MvPowerSeries.HasSubst, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
theorem
MvPowerSeries.hasSubst_of_constantCoeff_nilpotent
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Finite σ]
{a : σ → MvPowerSeries τ S}
(ha : ∀ (s : σ), IsNilpotent ((constantCoeff τ S) (a s)))
:
HasSubst a
If σ is finite, then the nilpotent condition is enough for HasSubst
theorem
MvPowerSeries.hasSubst_of_constantCoeff_zero
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Finite σ]
{a : σ → MvPowerSeries τ S}
(ha : ∀ (s : σ), (constantCoeff τ S) (a s) = 0)
:
HasSubst a
If σ is finite, then having zero constant coefficient is enough for HasSubst
noncomputable def
MvPowerSeries.subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
(a : σ → MvPowerSeries τ S)
(f : MvPowerSeries σ R)
:
MvPowerSeries τ S
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
theorem
MvPowerSeries.subst_eq_eval₂
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
:
theorem
MvPowerSeries.subst_coe
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(p : MvPolynomial σ R)
:
noncomputable def
MvPowerSeries.substAlgHom
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
:
For HasSubst a, MvPowerSeries.subst is an algebra morphism.
Equations
theorem
MvPowerSeries.substAlgHom_eq_aeval
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
(ha : HasSubst a)
:
Rewrite MvPowerSeries.substAlgHom as MvPowerSeries.aeval.
Its use is discouraged because it introduces a topology and might lead into awkward comparisons.
@[simp]
theorem
MvPowerSeries.coe_substAlgHom
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
:
@[simp]
theorem
MvPowerSeries.substAlgHom_apply
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(f : MvPowerSeries σ R)
:
theorem
MvPowerSeries.subst_smul
{σ : Type u_1}
{A : Type u_2}
[CommSemiring A]
{R : Type u_3}
[CommRing R]
[Algebra A R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra A S]
[Algebra R S]
[IsScalarTower A R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(r : A)
(f : MvPowerSeries σ R)
:
theorem
MvPowerSeries.substAlgHom_coe
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(p : MvPolynomial σ R)
:
theorem
MvPowerSeries.substAlgHom_X
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(s : σ)
:
theorem
MvPowerSeries.substAlgHom_monomial
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(e : σ →₀ ℕ)
(r : R)
:
(substAlgHom ha) ((monomial R e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun (s : σ) (n : ℕ) => a s ^ n
theorem
MvPowerSeries.subst_monomial
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(e : σ →₀ ℕ)
(r : R)
:
subst a ((monomial R e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun (s : σ) (n : ℕ) => a s ^ n
theorem
MvPowerSeries.continuous_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
:
Continuous (subst a)
theorem
MvPowerSeries.coeff_subst_finite
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(f : MvPowerSeries σ R)
(e : τ →₀ ℕ)
:
theorem
MvPowerSeries.coeff_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(f : MvPowerSeries σ R)
(e : τ →₀ ℕ)
:
theorem
MvPowerSeries.constantCoeff_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
(f : MvPowerSeries σ R)
:
theorem
MvPowerSeries.map_algebraMap_eq_subst_X
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{S : Type u_5}
[CommRing S]
[Algebra R S]
(f : MvPowerSeries σ R)
:
theorem
MvPowerSeries.comp_substAlgHom
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{T : Type u_6}
[CommRing T]
[UniformSpace T]
[T2Space T]
[CompleteSpace T]
[IsUniformAddGroup T]
[IsTopologicalRing T]
[IsLinearTopology T T]
[Algebra R T]
{ε : MvPowerSeries τ S →ₐ[R] T}
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
(ha : HasSubst a)
(hε : Continuous ⇑ε)
:
theorem
MvPowerSeries.comp_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{T : Type u_6}
[CommRing T]
[UniformSpace T]
[T2Space T]
[CompleteSpace T]
[IsUniformAddGroup T]
[IsTopologicalRing T]
[IsLinearTopology T T]
[Algebra R T]
{ε : MvPowerSeries τ S →ₐ[R] T}
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
(ha : HasSubst a)
(hε : Continuous ⇑ε)
:
theorem
MvPowerSeries.comp_subst_apply
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{T : Type u_6}
[CommRing T]
[UniformSpace T]
[T2Space T]
[CompleteSpace T]
[IsUniformAddGroup T]
[IsTopologicalRing T]
[IsLinearTopology T T]
[Algebra R T]
{ε : MvPowerSeries τ S →ₐ[R] T}
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
(ha : HasSubst a)
(hε : Continuous ⇑ε)
(f : MvPowerSeries σ R)
:
theorem
MvPowerSeries.eval₂_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{T : Type u_6}
[CommRing T]
[UniformSpace T]
[T2Space T]
[CompleteSpace T]
[IsUniformAddGroup T]
[IsTopologicalRing T]
[IsLinearTopology T T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
(ha : HasSubst a)
{b : τ → T}
(hb : HasEval b)
(f : MvPowerSeries σ R)
:
eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun (s : σ) => eval₂ (algebraMap S T) b (a s)) f
theorem
MvPowerSeries.IsNilpotent_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
(ha : HasSubst a)
{f : MvPowerSeries σ R}
(hf : IsNilpotent ((constantCoeff σ R) f))
:
IsNilpotent ((constantCoeff τ S) ((substAlgHom ha) f))
theorem
MvPowerSeries.HasSubst.comp
{σ : Type u_1}
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
{a : σ → MvPowerSeries τ S}
{υ : Type u_7}
{T : Type u_8}
[CommRing T]
[Algebra S T]
{b : τ → MvPowerSeries υ T}
(ha : HasSubst a)
(hb : HasSubst b)
:
HasSubst fun (s : σ) => (substAlgHom hb) (a s)
theorem
MvPowerSeries.substAlgHom_comp_substAlgHom
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{υ : Type u_7}
{T : Type u_8}
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{b : τ → MvPowerSeries υ T}
(ha : HasSubst a)
(hb : HasSubst b)
:
theorem
MvPowerSeries.substAlgHom_comp_substAlgHom_apply
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{υ : Type u_7}
{T : Type u_8}
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{b : τ → MvPowerSeries υ T}
(ha : HasSubst a)
(hb : HasSubst b)
(f : MvPowerSeries σ R)
:
theorem
MvPowerSeries.subst_comp_subst
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{υ : Type u_7}
{T : Type u_8}
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{b : τ → MvPowerSeries υ T}
(ha : HasSubst a)
(hb : HasSubst b)
:
theorem
MvPowerSeries.subst_comp_subst_apply
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
{τ : Type u_4}
{S : Type u_5}
[CommRing S]
[Algebra R S]
{a : σ → MvPowerSeries τ S}
{υ : Type u_7}
{T : Type u_8}
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{b : τ → MvPowerSeries υ T}
(ha : HasSubst a)
(hb : HasSubst b)
(f : MvPowerSeries σ R)
:
noncomputable def
MvPowerSeries.rescale
{σ : Type u_1}
{R : Type u_9}
[CommSemiring R]
(a : σ → R)
:
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.
@[simp]
theorem
MvPowerSeries.rescale_zero_apply
{σ : Type u_1}
{R : Type u_9}
[CommSemiring R]
(f : MvPowerSeries σ R)
:
@[simp]
theorem
MvPowerSeries.rescale_rescale
{σ : Type u_1}
{R : Type u_9}
[CommSemiring R]
(f : MvPowerSeries σ R)
(a b : σ → R)
:
theorem
MvPowerSeries.rescale_homogeneous_eq_smul
{σ : Type u_1}
{R : Type u_9}
[CommSemiring R]
{n : ℕ}
{r : R}
{f : MvPowerSeries σ R}
(hf : ∀ d ∈ Function.support f, d.degree = n)
:
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' := ⋯ }
noncomputable def
MvPowerSeries.rescaleAlgHom
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
(a : σ → R)
:
Rescale a multivariate power series, as an AlgHom in the scaling parameters,
by multiplying each variable x by the value a x.
Equations
theorem
MvPowerSeries.rescaleAlgHom_apply
{σ : Type u_1}
{R : Type u_3}
[CommRing R]
(a : σ → R)
(f : MvPowerSeries σ R)
: