English
Let f: M1 → M2 be a linear map of modules over a commutative semiring R, and let b1, b2 be bases (indexed by finite sets) of M1 and M2, respectively. After extending scalars along a commutative semiring A with an R-algebra structure, the matrix of f with respect to the A-extensions of these bases is obtained by applying the algebra map R → A entrywise to the original matrix of f.
Русский
Пусть f: M1 → M2 — линейное отображение модулей над R, и пусть b1, b2 — базисы модулов M1, M2 соответственно. После смены базиса до A, матрица отображения получается из исходной матрицы путём применения алгебраического отображения R → A по каждому элементу матрицы.
LaTeX
$$$\\operatorname{toMatrix} (\\mathrm{basis}\; A\\; b_1) (\\mathrm{basis}\\; A\\; b_2) (f.\\mathrm{baseChange}\\ A) = (\\operatorname{toMatrix} b_1 b_2 f).\\mathrm{map} (\\mathrm{algebraMap} \\; R \\; A)$$$
Lean4
@[simp]
theorem toMatrix_baseChange (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) :
toMatrix (basis A b₁) (basis A b₂) (f.baseChange A) = (toMatrix b₁ b₂ f).map (algebraMap R A) := by ext;
simp [toMatrix_apply]
