English
Let f be an R-linear map between modules with bases b1 and b2. For i in ι₂ and c a finitely supported function on ι₁ with values in R, the evaluation of the mv-polynomial corresponding to f at i with coefficient c equals the i-th coordinate of the representation of f applied to the vector determined by c in the basis b1.
Русский
Пусть f: M1 → M2 является линейным отображением над R между модулями с базами b1 и b2. Для i в ι₂ и для c ∈ ι₁ →₀ R, вычисление mv-полиномa f по i и c даёт i-ю координату представления f применённого к вектору, заданному коэффициентами c в базисе b1.
LaTeX
$$$\\operatorname{eval}_c\\bigl(f.toMvPolynomial_{b_1,b_2}(i)\\bigr) = b_2.repr\\Bigl(f\\bigl(b_1.repr^{-1}(c)\\bigr)\\Bigr)_i$$$
Lean4
/-- Let `f : M₁ →ₗ[R] M₂` be an `R`-linear map
between modules `M₁` and `M₂` with bases `b₁` and `b₂` respectively.
Then `LinearMap.toMvPolynomial b₁ b₂ f` is the family of multivariate polynomials over `R`
that evaluates on an element `x` of `M₁` (represented on the basis `b₁`)
to the element `f x` of `M₂` (represented on the basis `b₂`). -/
noncomputable def toMvPolynomial (f : M₁ →ₗ[R] M₂) (i : ι₂) : MvPolynomial ι₁ R :=
(toMatrix b₁ b₂ f).toMvPolynomial i
