Evaluation of a series in a subset of the coordinates

A convergent series f in d variables embedded along e : Fin d ↪ Fin n (convEmbed, MvPowerSeries.rename e) evaluates at x : Fin n → K to f evaluated at x ∘ e (evalSeries_rename): the coefficient of rename e f at a monomial is that of f at its preimage and vanishes off the image of Finsupp.embDomain e, and the monomial x^{embDomain e μ} is (x ∘ e)^μ. Used for the upper semicontinuity of the dimension: the base coefficients of a Noether normalization, read as functions on Kⁿ, depend only on the base coordinates (Parameters.lean, Reexpansion.lean).

theorem Analytic.monomialEval_embDomain {K : Type u_1} [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) (x : Fin n → K) (μ : Fin d →₀ ℕ) : monomialEval x (Finsupp.embDomain e μ) = monomialEval (x ∘ ⇑e) μ

The monomial x^{e(μ)} in the coordinates e i is the monomial (x ∘ e)^μ.

theorem Analytic.evalSeries_rename {K : Type u_1} [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) (f : MvPowerSeries (Fin d) K) (x : Fin n → K) : evalSeries ((MvPowerSeries.rename ⇑e) f) x = evalSeries f (x ∘ ⇑e)

Evaluating the series rename e f in the coordinates e i at x is evaluating f at x ∘ e: the sum over the monomials of rename e f is the sum over the monomials of f (coeff_embDomain_rename, coeff_rename_eq_zero).