English
If p.vars is contained in the range of f and f is injective, there exists q with rename f q = p.
Русский
Если множество переменных p находится внутри диапазона отображения f и f инъективно, существует q такой, что rename f q = p.
LaTeX
$$$ \exists q, rename\ f\ q = p $$$
Lean4
theorem exists_rename_eq_of_vars_subset_range (p : MvPolynomial σ R) (f : τ → σ) (hfi : Injective f)
(hf : ↑p.vars ⊆ Set.range f) : ∃ q : MvPolynomial τ R, rename f q = p :=
⟨aeval (fun i : σ => Option.elim' 0 X <| partialInv f i) p,
by
change (rename f).toRingHom.comp _ p = RingHom.id _ p
refine hom_congr_vars ?_ ?_ ?_
· ext1
simp [algebraMap_eq]
· intro i hip _
rcases hf hip with ⟨i, rfl⟩
simp [partialInv_left hfi]
· rfl⟩