This file defines the
comap function on
mv_polynomial.comap is a low-tech example of a map of "algebraic varieties," modulo the fact that
mathlib does not yet define varieties.
As in other polynomial files, we typically use the notation:
Given an algebra hom
f : mv_polynomial σ R →ₐ[R] mv_polynomial τ R
and a variable evaluation
v : τ → R,
comap f v produces a variable evaluation
σ → R.
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