Documentation

Mathlib.RingTheory.MvPowerSeries.Substitution

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:

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 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 #

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

Instances For
    theorem MvPowerSeries.hasSubst_def {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [CommRing S] (a : σMvPowerSeries τ S) :
    HasSubst a (∀ (s : σ), IsNilpotent ((constantCoeff τ S) (a s))) ∀ (d : τ →₀ ), {s : σ | (coeff S d) (a s) 0}.Finite
    theorem MvPowerSeries.coeff_zero_iff {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [CommRing S] {a : σMvPowerSeries τ S} [TopologicalSpace S] [DiscreteTopology S] :
    Filter.Tendsto a Filter.cofinite (nhds 0) ∀ (d : τ →₀ ), {s : σ | (coeff S d) (a s) 0}.Finite

    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) :
    theorem MvPowerSeries.HasSubst.zero {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [CommRing S] :
    HasSubst fun (x : σ) => 0
    theorem MvPowerSeries.HasSubst.add {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [CommRing S] {a b : σMvPowerSeries τ S} (ha : HasSubst a) (hb : HasSubst b) :
    HasSubst (a + b)
    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) :
    HasSubst (b * 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) :
    HasSubst (a * b)
    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) :
    theorem MvPowerSeries.HasSubst.X {σ : Type u_1} {S : Type u_5} [CommRing S] :
    HasSubst fun (s : σ) => X s
    theorem MvPowerSeries.HasSubst.smul_X {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σR) :
    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
    Instances For
      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))) :

      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) :

      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) :

      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
      Instances For
        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
        Instances For
          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) :
          (substAlgHom ha) = (aeval )

          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) :
          (substAlgHom ha) = subst a
          theorem MvPowerSeries.subst_self {σ : Type u_1} {R : Type u_3} [CommRing R] :
          @[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) :
          (substAlgHom ha) f = subst a f
          theorem MvPowerSeries.subst_add {σ : 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 g : MvPowerSeries σ R) :
          subst a (f + g) = subst a f + subst a g
          theorem MvPowerSeries.subst_mul {σ : 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 g : MvPowerSeries σ R) :
          subst a (f * g) = subst a f * subst a g
          theorem MvPowerSeries.subst_pow {σ : 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) (n : ) :
          subst a (f ^ n) = subst a f ^ n
          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) :
          subst a (r f) = r subst a f
          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 : σ) :
          (substAlgHom ha) (X s) = 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
          @[simp]
          theorem MvPowerSeries.subst_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 : σ) :
          subst a (X s) = a s
          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] :
          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 : τ →₀ ) :
          (Function.support fun (d : σ →₀ ) => (coeff R d) f (coeff S e) (d.prod fun (s : σ) (e : ) => a s ^ e)).Finite
          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 : τ →₀ ) :
          (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ), (coeff R d) f (coeff S e) (d.prod fun (s : σ) (e : ) => a s ^ 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) :
          (constantCoeff τ S) (subst a f) = ∑ᶠ (d : σ →₀ ), (coeff R d) f (constantCoeff τ S) (d.prod fun (s : σ) (e : ) => a s ^ e)
          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) :
          (map σ (algebraMap R S)) f = subst X f
          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) ( : Continuous ε) :
          ε.comp (substAlgHom ha) = aeval
          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) ( : Continuous ε) :
          ε subst a = (aeval )
          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) ( : Continuous ε) (f : MvPowerSeries σ R) :
          ε (subst a f) = (aeval ) f
          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)) :
          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) :
          (substAlgHom hb) ((substAlgHom ha) f) = (substAlgHom ) f
          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) :
          subst b subst a = subst fun (s : σ) => subst b (a s)
          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) :
          subst b (subst a f) = subst (fun (s : σ) => subst b (a s)) f
          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.
          Instances For
            @[simp]
            theorem MvPowerSeries.coeff_rescale {σ : Type u_1} {R : Type u_9} [CommSemiring R] (f : MvPowerSeries σ R) (a : σR) (n : σ →₀ ) :
            (coeff R n) ((rescale a) f) = (n.prod fun (s : σ) (m : ) => a s ^ m) * (coeff R n) f
            @[simp]
            theorem MvPowerSeries.rescale_zero {σ : Type u_1} {R : Type u_9} [CommSemiring R] :
            rescale 0 = (C σ R).comp (constantCoeff σ R)
            theorem MvPowerSeries.rescale_zero_apply {σ : Type u_1} {R : Type u_9} [CommSemiring R] (f : MvPowerSeries σ R) :
            (rescale 0) f = (C σ R) ((constantCoeff σ R) f)
            @[simp]
            theorem MvPowerSeries.rescale_rescale {σ : Type u_1} {R : Type u_9} [CommSemiring R] (f : MvPowerSeries σ R) (a b : σR) :
            (rescale b) ((rescale a) f) = (rescale (a * b)) f
            theorem MvPowerSeries.rescale_mul {σ : Type u_1} {R : Type u_9} [CommSemiring R] (a b : σR) :
            rescale (a * b) = (rescale b).comp (rescale a)
            theorem MvPowerSeries.rescale_homogeneous_eq_smul {σ : Type u_1} {R : Type u_9} [CommSemiring R] {n : } {r : R} {f : MvPowerSeries σ R} (hf : dFunction.support f, d.degree = n) :
            (rescale (Function.const σ r)) f = r ^ n f

            Rescaling a homogeneous power series

            noncomputable def MvPowerSeries.rescaleMonoidHom {σ : Type u_1} {R : Type u_9} [CommSemiring R] :
            (σR) →* MvPowerSeries σ R →+* MvPowerSeries σ R

            Rescale a multivariate power series, as a MonoidHom in the scaling parameters.

            Equations
            Instances For
              theorem MvPowerSeries.rescale_eq_subst {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σR) (f : MvPowerSeries σ R) :
              (rescale a) f = subst (a X) f
              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
              Instances For
                theorem MvPowerSeries.rescaleAlgHom_apply {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σR) (f : MvPowerSeries σ R) :
                (rescaleAlgHom a) f = (rescale a) f
                theorem MvPowerSeries.rescaleAlgHom_mul {σ : Type u_1} {R : Type u_3} [CommRing R] (a b : σR) :