Coefficients of products with powers of the ideal of the variables

Let J be the ideal of R[X_i : i ∈ σ] generated by the variables, so that J ^ k consists of the polynomials all of whose monomials have total degree at least k (MvPolynomial.mem_pow_idealOfVars_iff). This file records that multiplying an element of J ^ k by any q only involves the constant coefficient of q in total degrees at most k. This is how a linear map between free modules over R[X_i : i ∈ σ] acts, in the lowest degree of the J-adic filtration, through its reduction modulo the variables.

Main results

• MvPolynomial.coeff_mul_of_mem_pow_idealOfVars: for p ∈ J ^ k and a monomial e of total degree at most k, the coefficient of e in p * q is the coefficient of e in p times the constant coefficient of q.

theorem MvPolynomial.coeff_mul_of_mem_pow_idealOfVars {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) {k : ℕ} (hp : p ∈ idealOfVars σ R ^ k) (q : MvPolynomial σ R) {e : σ →₀ ℕ} (he : Finsupp.degree e ≤ k) : (p * q).coeff e = p.coeff e * constantCoeff q

If p lies in the k-th power of the ideal generated by the variables, then the coefficients of p * q in total degree at most k are those of p times the constant coefficient of q.