Documentation

Mathlib.RingTheory.MvPowerSeries.Basic

Formal (multivariate) power series #

This file defines multivariate formal power series and develops the basic properties of these objects.

A formal power series is to a polynomial like an infinite sum is to a finite sum.

We provide the natural inclusion from multivariate polynomials to multivariate formal power series.

Main definitions #

MvPowerSeries.C: constant power series
MvPowerSeries.X: the indeterminates
MvPowerSeries.coeff, MvPowerSeries.constantCoeff: the coefficients of a MvPowerSeries, its constant coefficient
MvPowerSeries.monomial: the monomials
MvPowerSeries.coeff_mul: computes the coefficients of the product of two MvPowerSeries
MvPowerSeries.coeff_prod : computes the coefficients of products of MvPowerSeries
MvPowerSeries.coeff_pow : computes the coefficients of powers of a MvPowerSeries
MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent: if the constant coefficient of a MvPowerSeries is nilpotent, then some coefficients of its powers are automatically zero
MvPowerSeries.map: apply a RingHom to the coefficients of a MvPowerSeries (as a `RingHom)
MvPowerSeries.X_pow_dvd_iff, MvPowerSeries.X_dvd_iff: equivalent conditions for (a power of) an indeterminate to divide a MvPowerSeries
MvPolynomial.toMvPowerSeries: the canonical coercion from MvPolynomial to MvPowerSeries

Note #

This file sets up the (semi)ring structure on multivariate power series: additional results are in:

Mathlib.RingTheory.MvPowerSeries.Inverse : invertibility, formal power series over a local ring form a local ring;
Mathlib.RingTheory.MvPowerSeries.Trunc: truncation of power series.

In Mathlib.RingTheory.PowerSeries.Basic, formal power series in one variable will be obtained as a particular case, defined by PowerSeries R := MvPowerSeries Unit R. See that file for a specific description.

Implementation notes #

In this file we define multivariate formal power series with variables indexed by σ and coefficients in R as MvPowerSeries σ R := (σ →₀ ℕ) → R. Unfortunately there is not yet enough API to show that they are the completion of the ring of multivariate polynomials. However, we provide most of the infrastructure that is needed to do this. Once I-adic completion (topological or algebraic) is available it should not be hard to fill in the details.

def MvPowerSeries (σ : Type u_1) (R : Type u_2) :

Type (max u_2 u_1)

Multivariate formal power series, where σ is the index set of the variables and R is the coefficient ring.

Equations

MvPowerSeries σ R = ((σ →₀ ℕ) → R)

Instances For

instance MvPowerSeries.instInhabited {σ : Type u_1} {R : Type u_2} [Inhabited R] :

Inhabited (MvPowerSeries σ R)

Equations

MvPowerSeries.instInhabited = { default := fun (x : σ →₀ ℕ) => default }

instance MvPowerSeries.instZero {σ : Type u_1} {R : Type u_2} [Zero R] :

Zero (MvPowerSeries σ R)

Equations

MvPowerSeries.instZero = Pi.instZero

instance MvPowerSeries.instAddMonoid {σ : Type u_1} {R : Type u_2} [AddMonoid R] :

AddMonoid (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddMonoid = Pi.addMonoid

instance MvPowerSeries.instAddGroup {σ : Type u_1} {R : Type u_2} [AddGroup R] :

AddGroup (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddGroup = Pi.addGroup

instance MvPowerSeries.instAddCommMonoid {σ : Type u_1} {R : Type u_2} [AddCommMonoid R] :

AddCommMonoid (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddCommMonoid = Pi.addCommMonoid

instance MvPowerSeries.instAddCommGroup {σ : Type u_1} {R : Type u_2} [AddCommGroup R] :

AddCommGroup (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddCommGroup = Pi.addCommGroup

instance MvPowerSeries.instNontrivial {σ : Type u_1} {R : Type u_2} [Nontrivial R] :

Nontrivial (MvPowerSeries σ R)

Equations

⋯ = ⋯

instance MvPowerSeries.instModule {σ : Type u_1} {R : Type u_2} {A : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] :

Module R (MvPowerSeries σ A)

Equations

MvPowerSeries.instModule = Pi.module (σ →₀ ℕ) (fun (a : σ →₀ ℕ) => A) R

instance MvPowerSeries.instIsScalarTower {σ : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S] [IsScalarTower R S A] :

IsScalarTower R S (MvPowerSeries σ A)

Equations

⋯ = ⋯

def MvPowerSeries.monomial {σ : Type u_1} (R : Type u_2) [Semiring R] (n : σ →₀ ℕ) :

R →ₗ[R] MvPowerSeries σ R

The nth monomial as multivariate formal power series: it is defined as the R-linear map from R to the semi-ring of multivariate formal power series associating to each a the map sending n : σ →₀ ℕ to the value a and sending all other x : σ →₀ ℕ different from n to 0.

Equations

MvPowerSeries.monomial R n = LinearMap.stdBasis R (fun (x : σ →₀ ℕ) => R) n

Instances For

def MvPowerSeries.coeff {σ : Type u_1} (R : Type u_2) [Semiring R] (n : σ →₀ ℕ) :

MvPowerSeries σ R →ₗ[R] R

The nth coefficient of a multivariate formal power series.

Equations

MvPowerSeries.coeff R n = LinearMap.proj n

Instances For

theorem MvPowerSeries.ext {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} {ψ : MvPowerSeries σ R} (h : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ) :

φ = ψ

Two multivariate formal power series are equal if all their coefficients are equal.

theorem MvPowerSeries.ext_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} {ψ : MvPowerSeries σ R} :

φ = ψ ↔ ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ

Two multivariate formal power series are equal if and only if all their coefficients are equal.

theorem MvPowerSeries.monomial_def {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ℕ) :

MvPowerSeries.monomial R n = LinearMap.stdBasis R (fun (x : σ →₀ ℕ) => R) n

theorem MvPowerSeries.coeff_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (a : R) :

(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = if m = n then a else 0

@[simp]

theorem MvPowerSeries.coeff_monomial_same {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (a : R) :

(MvPowerSeries.coeff R n) ((MvPowerSeries.monomial R n) a) = a

theorem MvPowerSeries.coeff_monomial_ne {σ : Type u_1} {R : Type u_2} [Semiring R] {m : σ →₀ ℕ} {n : σ →₀ ℕ} (h : m ≠ n) (a : R) :

(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = 0

theorem MvPowerSeries.eq_of_coeff_monomial_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {m : σ →₀ ℕ} {n : σ →₀ ℕ} {a : R} (h : (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) ≠ 0) :

m = n

@[simp]

theorem MvPowerSeries.coeff_comp_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) :

MvPowerSeries.coeff R n ∘ₗ MvPowerSeries.monomial R n = LinearMap.id

theorem MvPowerSeries.coeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) :

(MvPowerSeries.coeff R n) 0 = 0

instance MvPowerSeries.instOne {σ : Type u_1} {R : Type u_2} [Semiring R] :

One (MvPowerSeries σ R)

Equations

MvPowerSeries.instOne = { one := (MvPowerSeries.monomial R 0) 1 }

theorem MvPowerSeries.coeff_one {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) [DecidableEq σ] :

(MvPowerSeries.coeff R n) 1 = if n = 0 then 1 else 0

theorem MvPowerSeries.coeff_zero_one {σ : Type u_1} {R : Type u_2} [Semiring R] :

(MvPowerSeries.coeff R 0) 1 = 1

theorem MvPowerSeries.monomial_zero_one {σ : Type u_1} {R : Type u_2} [Semiring R] :

(MvPowerSeries.monomial R 0) 1 = 1

instance MvPowerSeries.instAddMonoidWithOne {σ : Type u_1} {R : Type u_2} [Semiring R] :

AddMonoidWithOne (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddMonoidWithOne = let __src := let_fun this := inferInstance; this; AddMonoidWithOne.mk ⋯ ⋯

instance MvPowerSeries.instMul {σ : Type u_1} {R : Type u_2} [Semiring R] :

Mul (MvPowerSeries σ R)

Equations

MvPowerSeries.instMul = { mul := fun (φ ψ : MvPowerSeries σ R) (n : σ →₀ ℕ) => ∑ p ∈ Finset.antidiagonal n, (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ }

theorem MvPowerSeries.coeff_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (ψ : MvPowerSeries σ R) [DecidableEq σ] :

(MvPowerSeries.coeff R n) (φ * ψ) = ∑ p ∈ Finset.antidiagonal n, (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ

theorem MvPowerSeries.zero_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :

0 * φ = 0

theorem MvPowerSeries.mul_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :

φ * 0 = 0

theorem MvPowerSeries.coeff_monomial_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :

(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a * φ) = if n ≤ m then a * (MvPowerSeries.coeff R (m - n)) φ else 0

theorem MvPowerSeries.coeff_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :

(MvPowerSeries.coeff R m) (φ * (MvPowerSeries.monomial R n) a) = if n ≤ m then (MvPowerSeries.coeff R (m - n)) φ * a else 0

theorem MvPowerSeries.coeff_add_monomial_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :

(MvPowerSeries.coeff R (m + n)) ((MvPowerSeries.monomial R m) a * φ) = a * (MvPowerSeries.coeff R n) φ

theorem MvPowerSeries.coeff_add_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :

(MvPowerSeries.coeff R (m + n)) (φ * (MvPowerSeries.monomial R n) a) = (MvPowerSeries.coeff R m) φ * a

@[simp]

theorem MvPowerSeries.commute_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) {a : R} {n : σ →₀ ℕ} :

Commute φ ((MvPowerSeries.monomial R n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((MvPowerSeries.coeff R m) φ) a

theorem MvPowerSeries.one_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :

1 * φ = φ

theorem MvPowerSeries.mul_one {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :

φ * 1 = φ

theorem MvPowerSeries.mul_add {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ : MvPowerSeries σ R) (φ₂ : MvPowerSeries σ R) (φ₃ : MvPowerSeries σ R) :

φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃

theorem MvPowerSeries.add_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ : MvPowerSeries σ R) (φ₂ : MvPowerSeries σ R) (φ₃ : MvPowerSeries σ R) :

(φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃

theorem MvPowerSeries.mul_assoc {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ : MvPowerSeries σ R) (φ₂ : MvPowerSeries σ R) (φ₃ : MvPowerSeries σ R) :

φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)

instance MvPowerSeries.instSemiring {σ : Type u_1} {R : Type u_2} [Semiring R] :

Semiring (MvPowerSeries σ R)

Equations

One or more equations did not get rendered due to their size.

instance MvPowerSeries.instCommSemiring {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

CommSemiring (MvPowerSeries σ R)

Equations

MvPowerSeries.instCommSemiring = let __src := let_fun this := inferInstance; this; CommSemiring.mk ⋯

instance MvPowerSeries.instRing {σ : Type u_1} {R : Type u_2} [Ring R] :

Ring (MvPowerSeries σ R)

Equations

MvPowerSeries.instRing = let __src := inferInstanceAs (Semiring (MvPowerSeries σ R)); let __src_1 := inferInstanceAs (AddCommGroup (MvPowerSeries σ R)); Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MvPowerSeries.instCommRing {σ : Type u_1} {R : Type u_2} [CommRing R] :

CommRing (MvPowerSeries σ R)

Equations

MvPowerSeries.instCommRing = let __src := inferInstanceAs (CommSemiring (MvPowerSeries σ R)); let __src_1 := inferInstanceAs (AddCommGroup (MvPowerSeries σ R)); CommRing.mk ⋯

theorem MvPowerSeries.monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (a : R) (b : R) :

(MvPowerSeries.monomial R m) a * (MvPowerSeries.monomial R n) b = (MvPowerSeries.monomial R (m + n)) (a * b)

def MvPowerSeries.C (σ : Type u_1) (R : Type u_2) [Semiring R] :

R →+* MvPowerSeries σ R

The constant multivariate formal power series.

Equations

MvPowerSeries.C σ R = let __src := MvPowerSeries.monomial R 0; { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem MvPowerSeries.monomial_zero_eq_C {σ : Type u_1} {R : Type u_2} [Semiring R] :

⇑(MvPowerSeries.monomial R 0) = ⇑(MvPowerSeries.C σ R)

theorem MvPowerSeries.monomial_zero_eq_C_apply {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) :

(MvPowerSeries.monomial R 0) a = (MvPowerSeries.C σ R) a

theorem MvPowerSeries.coeff_C {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ℕ) (a : R) :

(MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a) = if n = 0 then a else 0

theorem MvPowerSeries.coeff_zero_C {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) :

(MvPowerSeries.coeff R 0) ((MvPowerSeries.C σ R) a) = a

def MvPowerSeries.X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :

MvPowerSeries σ R

The variables of the multivariate formal power series ring.

Equations

MvPowerSeries.X s = (MvPowerSeries.monomial R (Finsupp.single s 1)) 1

Instances For

theorem MvPowerSeries.coeff_X {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ℕ) (s : σ) :

(MvPowerSeries.coeff R n) (MvPowerSeries.X s) = if n = Finsupp.single s 1 then 1 else 0

theorem MvPowerSeries.coeff_index_single_X {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (s : σ) (t : σ) :

(MvPowerSeries.coeff R (Finsupp.single t 1)) (MvPowerSeries.X s) = if t = s then 1 else 0

@[simp]

theorem MvPowerSeries.coeff_index_single_self_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :

(MvPowerSeries.coeff R (Finsupp.single s 1)) (MvPowerSeries.X s) = 1

theorem MvPowerSeries.coeff_zero_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :

(MvPowerSeries.coeff R 0) (MvPowerSeries.X s) = 0

theorem MvPowerSeries.commute_X {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) :

Commute φ (MvPowerSeries.X s)

theorem MvPowerSeries.X_def {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :

MvPowerSeries.X s = (MvPowerSeries.monomial R (Finsupp.single s 1)) 1

theorem MvPowerSeries.X_pow_eq {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) (n : ℕ) :

MvPowerSeries.X s ^ n = (MvPowerSeries.monomial R (Finsupp.single s n)) 1

theorem MvPowerSeries.coeff_X_pow {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) :

(MvPowerSeries.coeff R m) (MvPowerSeries.X s ^ n) = if m = Finsupp.single s n then 1 else 0

@[simp]

theorem MvPowerSeries.coeff_mul_C {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :

(MvPowerSeries.coeff R n) (φ * (MvPowerSeries.C σ R) a) = (MvPowerSeries.coeff R n) φ * a

@[simp]

theorem MvPowerSeries.coeff_C_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :

(MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a * φ) = a * (MvPowerSeries.coeff R n) φ

theorem MvPowerSeries.coeff_zero_mul_X {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) :

(MvPowerSeries.coeff R 0) (φ * MvPowerSeries.X s) = 0

theorem MvPowerSeries.coeff_zero_X_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) :

(MvPowerSeries.coeff R 0) (MvPowerSeries.X s * φ) = 0

def MvPowerSeries.constantCoeff (σ : Type u_1) (R : Type u_2) [Semiring R] :

MvPowerSeries σ R →+* R

The constant coefficient of a formal power series.

Equations

MvPowerSeries.constantCoeff σ R = let __src := MvPowerSeries.coeff R 0; { toFun := ⇑(MvPowerSeries.coeff R 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem MvPowerSeries.coeff_zero_eq_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] :

⇑(MvPowerSeries.coeff R 0) = ⇑(MvPowerSeries.constantCoeff σ R)

theorem MvPowerSeries.coeff_zero_eq_constantCoeff_apply {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :

(MvPowerSeries.coeff R 0) φ = (MvPowerSeries.constantCoeff σ R) φ

@[simp]

theorem MvPowerSeries.constantCoeff_C {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) :

(MvPowerSeries.constantCoeff σ R) ((MvPowerSeries.C σ R) a) = a

@[simp]

theorem MvPowerSeries.constantCoeff_comp_C {σ : Type u_1} {R : Type u_2} [Semiring R] :

(MvPowerSeries.constantCoeff σ R).comp (MvPowerSeries.C σ R) = RingHom.id R

theorem MvPowerSeries.constantCoeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] :

(MvPowerSeries.constantCoeff σ R) 0 = 0

theorem MvPowerSeries.constantCoeff_one {σ : Type u_1} {R : Type u_2} [Semiring R] :

(MvPowerSeries.constantCoeff σ R) 1 = 1

@[simp]

theorem MvPowerSeries.constantCoeff_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :

(MvPowerSeries.constantCoeff σ R) (MvPowerSeries.X s) = 0

theorem MvPowerSeries.isUnit_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (h : IsUnit φ) :

IsUnit ((MvPowerSeries.constantCoeff σ R) φ)

If a multivariate formal power series is invertible, then so is its constant coefficient.

theorem MvPowerSeries.coeff_smul {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) (n : σ →₀ ℕ) (a : R) :

(MvPowerSeries.coeff R n) (a • f) = a * (MvPowerSeries.coeff R n) f

theorem MvPowerSeries.smul_eq_C_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) (a : R) :

a • f = (MvPowerSeries.C σ R) a * f

theorem MvPowerSeries.X_inj {σ : Type u_1} {R : Type u_2} [Semiring R] [Nontrivial R] {s : σ} {t : σ} :

MvPowerSeries.X s = MvPowerSeries.X t ↔ s = t

def MvPowerSeries.map (σ : Type u_1) {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) :

MvPowerSeries σ R →+* MvPowerSeries σ S

The map between multivariate formal power series induced by a map on the coefficients.

Equations

MvPowerSeries.map σ f = { toFun := fun (φ : MvPowerSeries σ R) (n : σ →₀ ℕ) => f ((MvPowerSeries.coeff R n) φ), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem MvPowerSeries.map_id {σ : Type u_1} {R : Type u_2} [Semiring R] :

MvPowerSeries.map σ (RingHom.id R) = RingHom.id (MvPowerSeries σ R)

theorem MvPowerSeries.map_comp {σ : Type u_1} {R : Type u_2} {S : Type u_3} {T : Type u_4} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) :

MvPowerSeries.map σ (g.comp f) = (MvPowerSeries.map σ g).comp (MvPowerSeries.map σ f)

@[simp]

theorem MvPowerSeries.coeff_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) :

(MvPowerSeries.coeff S n) ((MvPowerSeries.map σ f) φ) = f ((MvPowerSeries.coeff R n) φ)

@[simp]

theorem MvPowerSeries.constantCoeff_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (φ : MvPowerSeries σ R) :

(MvPowerSeries.constantCoeff σ S) ((MvPowerSeries.map σ f) φ) = f ((MvPowerSeries.constantCoeff σ R) φ)

@[simp]

theorem MvPowerSeries.map_monomial {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (n : σ →₀ ℕ) (a : R) :

(MvPowerSeries.map σ f) ((MvPowerSeries.monomial R n) a) = (MvPowerSeries.monomial S n) (f a)

@[simp]

theorem MvPowerSeries.map_C {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (a : R) :

(MvPowerSeries.map σ f) ((MvPowerSeries.C σ R) a) = (MvPowerSeries.C σ S) (f a)

@[simp]

theorem MvPowerSeries.map_X {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (s : σ) :

(MvPowerSeries.map σ f) (MvPowerSeries.X s) = MvPowerSeries.X s

theorem MvPowerSeries.X_pow_dvd_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {s : σ} {n : ℕ} {φ : MvPowerSeries σ R} :

MvPowerSeries.X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s < n → (MvPowerSeries.coeff R m) φ = 0

theorem MvPowerSeries.X_dvd_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {s : σ} {φ : MvPowerSeries σ R} :

MvPowerSeries.X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (MvPowerSeries.coeff R m) φ = 0

theorem MvPowerSeries.coeff_prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_4} [DecidableEq ι] [DecidableEq σ] (f : ι → MvPowerSeries σ R) (d : σ →₀ ℕ) (s : Finset ι) :

(MvPowerSeries.coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff R (l i)) (f i)

Coefficients of a product of power series

theorem MvPowerSeries.coeff_pow {σ : Type u_1} {R : Type u_3} [CommSemiring R] [DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ} (d : σ →₀ ℕ) :

(MvPowerSeries.coeff R d) (f ^ n) = ∑ l ∈ (Finset.range n).finsuppAntidiag d, ∏ i ∈ Finset.range n, (MvPowerSeries.coeff R (l i)) f

The dth coefficient of a power of a multivariate power series is the sum, indexed by finsuppAntidiag (Finset.range n) d, of products of coefficients

theorem MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent {σ : Type u_1} {R : Type u_3} [CommSemiring R] [DecidableEq σ] {f : MvPowerSeries σ R} {m : ℕ} (hf : (MvPowerSeries.constantCoeff σ R) f ^ m = 0) {d : σ →₀ ℕ} {n : ℕ} (hn : m + d.degree ≤ n) :

(MvPowerSeries.coeff R d) (f ^ n) = 0

Vanishing of coefficients of powers of multivariate power series when the constant coefficient is nilpotent [N. Bourbaki, Algebra {II}, Chapter 4, §4, n°2, proposition 3][bourbaki1981]

instance MvPowerSeries.instAlgebra {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

Algebra R (MvPowerSeries σ A)

Equations

MvPowerSeries.instAlgebra = let __src := let_fun this := inferInstance; this; Algebra.mk ((MvPowerSeries.map σ (algebraMap R A)).comp (MvPowerSeries.C σ R)) ⋯ ⋯

theorem MvPowerSeries.c_eq_algebraMap {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

MvPowerSeries.C σ R = algebraMap R (MvPowerSeries σ R)

theorem MvPowerSeries.algebraMap_apply {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {r : R} :

(algebraMap R (MvPowerSeries σ A)) r = (MvPowerSeries.C σ A) ((algebraMap R A) r)

instance MvPowerSeries.instNontrivialSubalgebraOfNonempty {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nonempty σ] [Nontrivial R] :

Nontrivial (Subalgebra R (MvPowerSeries σ R))

Equations

⋯ = ⋯

def MvPolynomial.toMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

MvPolynomial σ R → MvPowerSeries σ R

The natural inclusion from multivariate polynomials into multivariate formal power series.

Equations

↑φ n = MvPolynomial.coeff n φ

Instances For

instance MvPolynomial.coeToMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

Coe (MvPolynomial σ R) (MvPowerSeries σ R)

The natural inclusion from multivariate polynomials into multivariate formal power series.

Equations

MvPolynomial.coeToMvPowerSeries = { coe := MvPolynomial.toMvPowerSeries }

theorem MvPolynomial.coe_def {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :

↑φ = fun (n : σ →₀ ℕ) => MvPolynomial.coeff n φ

@[simp]

theorem MvPolynomial.coeff_coe {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (n : σ →₀ ℕ) :

(MvPowerSeries.coeff R n) ↑φ = MvPolynomial.coeff n φ

@[simp]

theorem MvPolynomial.coe_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (a : R) :

↑((MvPolynomial.monomial n) a) = (MvPowerSeries.monomial R n) a

@[simp]

theorem MvPolynomial.coe_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

↑0 = 0

@[simp]

theorem MvPolynomial.coe_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

↑1 = 1

@[simp]

theorem MvPolynomial.coe_add {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (ψ : MvPolynomial σ R) :

↑(φ + ψ) = ↑φ + ↑ψ

@[simp]

theorem MvPolynomial.coe_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (ψ : MvPolynomial σ R) :

↑(φ * ψ) = ↑φ * ↑ψ

@[simp]

theorem MvPolynomial.coe_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : R) :

↑(MvPolynomial.C a) = (MvPowerSeries.C σ R) a

@[simp]

theorem MvPolynomial.coe_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ) :

↑(MvPolynomial.X s) = MvPowerSeries.X s

theorem MvPolynomial.coe_injective (σ : Type u_1) (R : Type u_2) [CommSemiring R] :

Function.Injective Coe.coe

@[simp]

theorem MvPolynomial.coe_inj {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} :

↑φ = ↑ψ ↔ φ = ψ

@[simp]

theorem MvPolynomial.coe_eq_zero_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} :

↑φ = 0 ↔ φ = 0

@[simp]

theorem MvPolynomial.coe_eq_one_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} :

↑φ = 1 ↔ φ = 1

def MvPolynomial.coeToMvPowerSeries.ringHom {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

MvPolynomial σ R →+* MvPowerSeries σ R

The coercion from multivariate polynomials to multivariate power series as a ring homomorphism.

Equations

MvPolynomial.coeToMvPowerSeries.ringHom = { toFun := Coe.coe, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem MvPolynomial.coe_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} (n : ℕ) :

↑(φ ^ n) = ↑φ ^ n

@[simp]

theorem MvPolynomial.coeToMvPowerSeries.ringHom_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :

MvPolynomial.coeToMvPowerSeries.ringHom φ = ↑φ

def MvPolynomial.coeToMvPowerSeries.algHom {σ : Type u_1} {R : Type u_2} [CommSemiring R] (A : Type u_3) [CommSemiring A] [Algebra R A] :

MvPolynomial σ R →ₐ[R] MvPowerSeries σ A

The coercion from multivariate polynomials to multivariate power series as an algebra homomorphism.

Equations

MvPolynomial.coeToMvPowerSeries.algHom A = let __src := (MvPowerSeries.map σ (algebraMap R A)).comp MvPolynomial.coeToMvPowerSeries.ringHom; { toRingHom := __src, commutes' := ⋯ }

Instances For

@[simp]

theorem MvPolynomial.coeToMvPowerSeries.algHom_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (A : Type u_3) [CommSemiring A] [Algebra R A] :

(MvPolynomial.coeToMvPowerSeries.algHom A) φ = (MvPowerSeries.map σ (algebraMap R A)) ↑φ

instance MvPowerSeries.algebraMvPolynomial {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] :

Algebra (MvPolynomial σ R) (MvPowerSeries σ A)

Equations

MvPowerSeries.algebraMvPolynomial = (MvPolynomial.coeToMvPowerSeries.algHom A).toAlgebra

instance MvPowerSeries.algebraMvPowerSeries {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] :

Algebra (MvPowerSeries σ R) (MvPowerSeries σ A)

Equations

MvPowerSeries.algebraMvPowerSeries = (MvPowerSeries.map σ (algebraMap R A)).toAlgebra

theorem MvPowerSeries.algebraMap_apply' {σ : Type u_1} {R : Type u_2} (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] (p : MvPolynomial σ R) :

(algebraMap (MvPolynomial σ R) (MvPowerSeries σ A)) p = (MvPowerSeries.map σ (algebraMap R A)) ↑p

theorem MvPowerSeries.algebraMap_apply'' {σ : Type u_1} {R : Type u_2} (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] (f : MvPowerSeries σ R) :

(algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A)) f = (MvPowerSeries.map σ (algebraMap R A)) f