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 seriesMvPowerSeries.X
: the indeterminatesMvPowerSeries.coeff
,MvPowerSeries.constantCoeff
: the coefficients of aMvPowerSeries
, its constant coefficientMvPowerSeries.monomial
: the monomialsMvPowerSeries.coeff_mul
: computes the coefficients of the product of twoMvPowerSeries
MvPowerSeries.coeff_prod
: computes the coefficients of products ofMvPowerSeries
MvPowerSeries.coeff_pow
: computes the coefficients of powers of aMvPowerSeries
MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
: if the constant coefficient of aMvPowerSeries
is nilpotent, then some coefficients of its powers are automatically zeroMvPowerSeries.map
: apply aRingHom
to the coefficients of aMvPowerSeries
(as a `RingHom)MvPowerSeries.X_pow_dvd_iff
,MvPowerSeries.X_dvd_iff
: equivalent conditions for (a power of) an indeterminate to divide aMvPowerSeries
MvPolynomial.toMvPowerSeries
: the canonical coercion fromMvPolynomial
toMvPowerSeries
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.
Multivariate formal power series, where σ
is the index set of the variables
and R
is the coefficient ring.
Equations
- MvPowerSeries σ R = ((σ →₀ ℕ) → R)
Instances For
Equations
- MvPowerSeries.instZero = Pi.instZero
Equations
- MvPowerSeries.instAddMonoid = Pi.addMonoid
Equations
- MvPowerSeries.instAddGroup = Pi.addGroup
Equations
- MvPowerSeries.instAddCommMonoid = Pi.addCommMonoid
Equations
- MvPowerSeries.instAddCommGroup = Pi.addCommGroup
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The n
th 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.single R (fun (x : σ →₀ ℕ) => R) n
Instances For
The n
th coefficient of a multivariate formal power series.
Equations
Instances For
Two multivariate formal power series are equal if and only if all their coefficients are equal.
Two multivariate formal power series are equal if all their coefficients are equal.
Equations
- MvPowerSeries.instOne = { one := (MvPowerSeries.monomial R 0) 1 }
Equations
- MvPowerSeries.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯
Equations
- MvPowerSeries.instMul = { mul := fun (φ ψ : MvPowerSeries σ R) (n : σ →₀ ℕ) => ∑ p ∈ Finset.antidiagonal n, (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ }
Equations
- MvPowerSeries.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯
Equations
- MvPowerSeries.instCommSemiring = CommSemiring.mk ⋯
Equations
- MvPowerSeries.instCommRing = CommRing.mk ⋯
The constant multivariate formal power series.
Equations
- MvPowerSeries.C σ R = { toFun := (MvPowerSeries.monomial R 0).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The variables of the multivariate formal power series ring.
Equations
- MvPowerSeries.X s = (MvPowerSeries.monomial R (Finsupp.single s 1)) 1
Instances For
The constant coefficient of a formal power series.
Equations
- MvPowerSeries.constantCoeff σ R = { toFun := ⇑(MvPowerSeries.coeff R 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
If a multivariate formal power series is invertible, then so is its constant coefficient.
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
Coefficients of a product of power series
The d
th coefficient of a power of a multivariate power series
is the sum, indexed by finsuppAntidiag (Finset.range n) d
, of products of coefficients
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]
Equations
- MvPowerSeries.instAlgebra = Algebra.mk ((MvPowerSeries.map σ (algebraMap R A)).comp (MvPowerSeries.C σ R)) ⋯ ⋯
Equations
- ⋯ = ⋯
The natural inclusion from multivariate polynomials into multivariate formal power series.
Equations
- ↑φ n = MvPolynomial.coeff n φ
Instances For
The natural inclusion from multivariate polynomials into multivariate formal power series.
Equations
- MvPolynomial.coeToMvPowerSeries = { coe := MvPolynomial.toMvPowerSeries }
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
The coercion from multivariate polynomials to multivariate power series as an algebra homomorphism.
Equations
- MvPolynomial.coeToMvPowerSeries.algHom A = { toRingHom := (MvPowerSeries.map σ (algebraMap R A)).comp MvPolynomial.coeToMvPowerSeries.ringHom, commutes' := ⋯ }
Instances For
Equations
- MvPowerSeries.algebraMvPolynomial = (MvPolynomial.coeToMvPowerSeries.algHom A).toAlgebra
Equations
- MvPowerSeries.algebraMvPowerSeries = (MvPowerSeries.map σ (algebraMap R A)).toAlgebra