English
Given a family of generators P : Generators R S ι′ and an equivalence e : ι ≃ ι′, one obtains a new generators family on ι by composing with e, with σ′ given by renaming along e and aVAL adjusted accordingly; the val map is P.val ∘ e and the aevalVal_σ′ property follows from P.
Русский
Для семейства генераторов P и эквивалентности e: ι ≃ ι′ образуется новое семейство генераторов на индексе ι, через композицию с e; отображение σ′ задаётся переименованием вдоль e, а val и aevalVal_σ′ трактуются соответственно.
LaTeX
$$$\\exists P' : \\text{Generators } R S ι,\\; P' = P.\\text{reindex} \\\\ (e : ι \\simeq ι'),\\; \\text{val}_{P'} = P.{val} \\circ e,\\; P'.{σ} = \\mathrm{rename}\, e^{-1} \\circ P.{σ}$$$
Lean4
/-- Given generators `P` and an equivalence `ι ≃ P.vars`, these
are the induced generators indexed by `ι`. -/
noncomputable def reindex (P : Generators R S ι') (e : ι ≃ ι') : Generators R S ι
where
val := P.val ∘ e
σ' := rename e.symm ∘ P.σ
aeval_val_σ'
s := by
conv_rhs => rw [← P.aeval_val_σ s]
rw [← MvPolynomial.aeval_rename]
simp
