Expand multivariate power series

Given a multivariate power series φ, one may replace every occurrence of X i by X i ^ n, for some nonzero natural number n. This operation is called MvPowerSeries.expand and it is an algebra homomorphism.

Main declaration

• MvPowerSeries.expand: expand a multi variate power series by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

noncomputable def MvPowerSeries.expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) : MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R

Expand the power series by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

See also PowerSeries.expand.

Equations

• MvPowerSeries.expand p hp = MvPowerSeries.substAlgHom ⋯

theorem MvPowerSeries.expand_C {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (r : R) : (expand p hp) (C r) = C r

@[simp]

theorem MvPowerSeries.expand_X {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (i : σ) : (expand p hp) (X i) = X i ^ p

@[simp]

theorem MvPowerSeries.expand_monomial {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (d : σ →₀ ℕ) (r : R) : (expand p hp) ((monomial d) r) = (monomial (p • d)) r

@[simp]

theorem MvPowerSeries.expand_one {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] : expand 1 ⋯ = AlgHom.id R (MvPowerSeries σ R)

theorem MvPowerSeries.expand_one_apply {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (f : MvPowerSeries σ R) : (expand 1 ⋯) f = f

@[simp]

theorem MvPowerSeries.map_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} [Finite σ] [CommRing R] [CommRing S] (p : ℕ) (hp : p ≠ 0) (f : R →+* S) (φ : MvPowerSeries σ R) : (map f) ((expand p hp) φ) = (expand p hp) ((map f) φ)

theorem MvPowerSeries.HasSubst.expand {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [Finite τ] [CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S} (hf : HasSubst f) : HasSubst fun (i : σ) => (MvPowerSeries.expand p hp) (f i)

theorem MvPowerSeries.expand_comp_substAlgHom {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [Finite τ] [CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S} (hf : HasSubst f) : (expand p hp).comp (substAlgHom hf) = substAlgHom ⋯

theorem MvPowerSeries.expand_substAlgHom {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [Finite τ] [CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S} (hf : HasSubst f) {φ : MvPowerSeries σ S} : (expand p hp) ((substAlgHom hf) φ) = (substAlgHom ⋯) φ

theorem MvPowerSeries.expand_mul_eq_comp {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0) : expand (p * q) ⋯ = (expand p hp).comp (expand q hq)

theorem MvPowerSeries.expand_mul {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0) (φ : MvPowerSeries σ R) : (expand (p * q) ⋯) φ = (expand p hp) ((expand q hq) φ)

@[simp]

theorem MvPowerSeries.coeff_expand_smul {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) (m : σ →₀ ℕ) : (coeff (p • m)) ((expand p hp) φ) = (coeff m) φ

theorem MvPowerSeries.coeff_expand_of_not_dvd {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) {m : σ →₀ ℕ} {i : σ} (h : ¬p ∣ m i) : (coeff m) ((expand p hp) φ) = 0

theorem MvPowerSeries.support_expand_subset {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) : Function.support ((expand p hp) φ) ⊆ (fun (x : σ →₀ ℕ) => p • x) '' Function.support φ

theorem MvPowerSeries.support_expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) : Function.support ((expand p hp) φ) = (fun (x : σ →₀ ℕ) => p • x) '' Function.support φ