Renaming the variables of a multivariate power series #
Gaps in Mathlib's rename API, in three groups. The first compares a renaming with another
operation on the same series — substitution, evaluation, or reading a single-variable
coefficient — together with one consequence of those comparisons: that reindexing a two-variable
series along unitSumUnitEquivFinTwo carries an associativity identity with it. The second says
where a renamed series vanishes: at every exponent that is nonzero at a variable outside the
image of the renaming. The third is about two renamings at once — along embeddings with disjoint
images, a common value forces both series to be the same constant.
Substituting after renaming is the substitution along the renamed index, and evaluating after
renaming is the evaluation at the reindexed family: Mathlib has all these operations and the law
that lets them be compared — rename_eq_subst, which says a renaming is the substitution
sending each variable to a variable — but not the comparisons themselves, which is what a caller
reindexing a series needs.
Reading the coefficient of a single-variable monomial through a renaming along an embedding is
likewise available only through coeff_embDomain_rename, which speaks about Finsupp.embDomain;
at one variable raised to an arbitrary power the single (e i) n spelling is the more usable one.
When the target variable type is Unit, the renamed series is a univariate PowerSeries, and
the same coefficient is recorded in the PowerSeries.coeff spelling.
Associativity is where the two spellings of a two-variable series genuinely diverge: the named
form substitutes an already-substituted series through pairSubstitution, the Fin 2 form
through a Matrix.cons family over Fin 3. Transporting the identity therefore means
reindexing the three-variable ambient ring as well, along unitSumUnitSumUnitEquivFinThree.
Main results #
MvPowerSeries.subst_rename: substituting intorename e preindexes the family, i.e. it is substitutingg ∘ eintop.MvPowerSeries.coeff_single_rename: the coefficient ofrename e pat the single-variable monomialsingle (e i) nis the coefficient ofpatsingle i n, for any exponentn.PowerSeries.coeff_rename: renaming the variables ofpalonge : σ ≃ Unitgives a univariate power series whosen-th coefficient is that ofpatsingle (e.symm ()) n.MvPowerSeries.aeval_rename: evaluatingrename e pat a family reindexes the family, i.e. it is evaluatingpat that family precomposed withe.MvPowerSeries.rename_unitSumUnitEquivFinTwo_assoc: reindexing a two-variable associative series fromUnit ⊕ UnittoFin 2preserves its associativity identity.MvPowerSeries.coeff_rename_eq_zero_of_apply_ne_zero: a renamed series vanishes at every exponent that is nonzero at a variable outside the image of the renaming.MvPowerSeries.eq_C_of_rename_eq_renameandMvPowerSeries.right_eq_C_of_rename_eq_rename: renamings along embeddings with disjoint images agree only when both series are the same constant.
Provenance #
No external source. The first three statements are gaps in Mathlib's MvPowerSeries API and each
proof is a few steps of that same API; the fourth is the reindexing they were extracted for, and
its proof rewrites both sides of the identity through the three-variable renaming. The vanishing
and disjointness lemmas are likewise gaps in that API. All of them are recorded here rather than
inside their callers because they carry no content beyond rename.
A single-variable monomial's coefficient survives a renaming along an embedding, for any
exponent n. Mathlib's coeff_embDomain_rename states this through Finsupp.embDomain; at one
variable the single (e i) n spelling is the one a caller meets.
A series renamed onto the variable type Unit is read as a univariate power series: its
n-th PowerSeries coefficient is the coefficient of p at the n-th power of the variable
e.symm (). This is MvPowerSeries.coeff_single_rename in the PowerSeries.coeff spelling that
Mathlib's univariate API uses.
A renamed series has no exponent outside the image of e: if ν is nonzero at a variable
j that e misses, then ν is not in the range of Finsupp.mapDomain e, so the coefficient
vanishes. This is Mathlib's MvPowerSeries.coeff_rename_eq_zero with the witness of
non-membership supplied by a single variable.
Renamings along embeddings with disjoint images agree only on constants: if
rename e₁ a = rename e₂ b and no e₁ i is an e₂ j, then a is the constant series at its own
constant coefficient. MvPowerSeries.right_eq_C_of_rename_eq_rename is the companion for b,
which is the constant series at the same constant. The two series need not be indexed by the
same type: only the images of e₁ and e₂ inside τ have to be disjoint.
Both sides are the same constant: the companion of
MvPowerSeries.eq_C_of_rename_eq_rename for b. Reading the constant coefficient through the
renamings identifies the two constants, so the two series are equal as well.
Substituting into a renamed series reindexes the family: rename e p followed by
substituting g is p with g ∘ e substituted.
Both hypotheses are the ones the two operations already carry: rename needs e to have finite
fibres (TendstoCofinite) for the renamed coefficients to be well defined, and subst needs
HasSubst g. Nothing is assumed about e beyond that — in particular it need not be injective,
since a collision merely substitutes the same series for two variables.
Reindexing an associative two-variable series from Unit ⊕ Unit to Fin 2 preserves
associativity in Mathlib's three-variable convention.
The source identity uses the named left, middle, and right variables supplied by the nested sum;
the target is exactly the identity expected by FormalGroup.assoc.
Evaluating a renamed series reindexes the family: evaluating rename e p at a is
evaluating p at a precomposed with e. This is the evaluation counterpart of subst_rename,
and Mathlib has neither.
The reindexed family is a separate argument b together with the pointwise equation
b s = a (e s), rather than the composite a ∘ e itself, because aeval carries its family in
the type of its HasEval argument: a caller who knows the reindexed family in a simplified form
cannot rewrite it under aeval afterwards, and supplying it here is the only way to state the
evaluation it actually wants.