English
If two polynomial types over the same coefficient ring are algebraically equivalent, there is a bijection between the sets of coefficient functions, induced by comap with the equivalence and its inverse.
Русский
Если два типа полиномов над одним кольцом R эквивалентны как алгебра, существует биекция между множествами функций-коэффициентов, индуцированная comap через эквивалент и его обратный.
LaTeX
$$$\\text{comapEquiv } f : (\\tau \\to R) \\simeq (\\sigma \\to R)$$$
Lean4
/-- If two polynomial types over the same coefficient ring `R` are equivalent,
there is a bijection between the types of functions from their variable types to `R`.
-/
noncomputable def comapEquiv (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R) : (τ → R) ≃ (σ → R)
where
toFun := comap f
invFun := comap f.symm
left_inv := by
intro x
rw [← comap_comp_apply]
apply comap_eq_id_of_eq_id
intro
simp only [AlgHom.id_apply, AlgEquiv.comp_symm]
right_inv := by
intro x
rw [← comap_comp_apply]
apply comap_eq_id_of_eq_id
intro
simp only [AlgHom.id_apply, AlgEquiv.symm_comp]
