English
The finSuccEquiv construction commutes with a renaming of indices via an equivalence, up to composing with a standard left renaming.
Русский
Конструкция finSuccEquiv коммутирует с переименованием индексов через эквиваленцию, до композиции с обычным левым переименованием.
LaTeX
$$$\bigl(\mathrm{finSuccEquiv}(R,n)\bigl)(\mathrm{rename}\bigl((\mathrm{Equiv.optionCongr}\ e).trans(\mathrm{finSuccEquiv}\ n).symm\bigr) \phi\bigr) = \mathrm{Polynomial.map}(\mathrm{rename}\,e).toRingHom(\mathrm{optionEquivLeft}\;R\;\sigma\;\phi)$$$
Lean4
/-- Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`,
and suppose that `σ ≃ Fin n`.
Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by
1. renaming the variables via `Option σ ≃ Fin (n+1)`, and then singling out the `0`-th variable
via `MvPolynomial.finSuccEquiv`;
2. first viewing it as polynomial over `MvPolynomial σ R` via `MvPolynomial.optionEquivLeft`,
and then renaming the variables.
This lemma shows that both constructions are the same. -/
theorem finSuccEquiv_rename_finSuccEquiv (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) :
((finSuccEquiv R n) ((rename ((Equiv.optionCongr e).trans (_root_.finSuccEquiv n).symm)) φ)) =
Polynomial.map (rename e).toRingHom (optionEquivLeft R σ φ) :=
by
suffices
(finSuccEquiv R n).toRingEquiv.toRingHom.comp
(rename ((Equiv.optionCongr e).trans (_root_.finSuccEquiv n).symm)).toRingHom =
(Polynomial.mapRingHom (rename e).toRingHom).comp (optionEquivLeft R σ)
by exact DFunLike.congr_fun this φ
apply ringHom_ext
· simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply, optionEquivLeft_apply]
· rintro (i | i) <;> simp [finSuccEquiv_apply, optionEquivLeft_apply]
