English
If f is a linear map and A is a commutative ring with R-algebra structure, then the mv-polynomial of the base-changed map equals the base-change of the mv-polynomial of f, i.e., (f.baseChange A).toMvPolynomial commutes with the map algebraMap from R to A.
Русский
Пусть f: M1 → M2 линейно над R, и A — кольцо с структурой алгебры над R. Тогда mv-полином базового перехода (baseChange) для f равен образу mv-полynomials через алгебра maps: (f.baseChange A).toMvPolynomial = MvPolynomial.map(algebraMap) (f.toMvPolynomial).
LaTeX
$$$ (f.baseChange A).toMvPolynomial (basis A b_1) (basis A b_2) i = MvPolynomial.map (algebraMap R A) (f.toMvPolynomial b_1 b_2 i) $$$
Lean4
theorem toMvPolynomial_baseChange (f : M₁ →ₗ[R] M₂) (i : ι₂) (A : Type*) [CommRing A] [Algebra R A] :
(f.baseChange A).toMvPolynomial (basis A b₁) (basis A b₂) i =
MvPolynomial.map (algebraMap R A) (f.toMvPolynomial b₁ b₂ i) :=
by simp only [toMvPolynomial, toMatrix_baseChange, Matrix.toMvPolynomial_map]
