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.

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_subst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [Finite τ] [CommRing R] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ R} (hf : HasSubst f) {φ : MvPowerSeries σ R} : (expand p hp) (subst f φ) = subst (fun (i : σ) => (expand p hp) (f i)) φ

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

@[simp]

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

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 φ

@[simp]

theorem MvPowerSeries.order_expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) : ((expand p hp) φ).order = p • φ.order

@[simp]

theorem MvPowerSeries.expand_eq_expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) {φ : MvPolynomial σ R} : (expand p hp) ↑φ = ↑((MvPolynomial.expand p) φ)

For any multivariate polynomial φ, then MvPolynomial.expand p φ and MvPowerSeries.expand p hp ↑φ coincide.

theorem MvPowerSeries.trunc'_expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) [DecidableEq σ] {n : σ →₀ ℕ} (φ : MvPowerSeries σ R) : (trunc' R (p • n)) ((expand p hp) φ) = (MvPolynomial.expand p) ((trunc' R n) φ)

theorem MvPowerSeries.trunc'_expand_trunc' {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) {n m : σ →₀ ℕ} (h : n ≤ m) [DecidableEq σ] (f : MvPowerSeries σ R) : (MvPolynomial.expand p) ((trunc' R n) f) = (trunc' R (p • n)) ↑((MvPolynomial.expand p) ((trunc' R m) f))

theorem MvPowerSeries.map_frobenius_expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) [ExpChar R p] {f : MvPowerSeries σ R} : (map (frobenius R p)) ((expand p hp) f) = f ^ p

theorem MvPowerSeries.map_iterateFrobenius_expand {σ : Type u_1} {R : Type u_3} [Finite σ] [CommRing R] (p : ℕ) (hp : p ≠ 0) [ExpChar R p] (f : MvPowerSeries σ R) (n : ℕ) : (map (iterateFrobenius R p n)) ((expand (p ^ n) ⋯) f) = f ^ p ^ n