English
For a family of vectors v_i in a module M, the matrix formed from these vectors after restricting scalars along an algebra map equals the matrix formed from the restricted vectors after applying the map to their coordinates.
Русский
Для семейства векторов v_i в модуле M матрица, составленная из этих векторов после ограничения скаляров вдоль алгебраического отображения, равна матрице, полученной из ограниченных векторов после применения отображения к их координатам.
LaTeX
$$$\\big(\\text{algebraMap } R_2 \\!\\to\\! S\\big).\\mathrm{mapMatrix}\\big( b.restrictScalars\\, R_2\\,\\text{toMatrix } v\\big) = b.toMatrix\\big(\\lambda i. (v(i))\\!\\text{.val}\\big)$$$
Lean4
/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,
and matrices, making the matrix whose columns are the vectors `v i` written in the basis `e`. -/
def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix ι ι R
where
toFun := e.toMatrix
map_add' v
w := by
ext i j
rw [Matrix.add_apply, e.toMatrix_apply, Pi.add_apply, LinearEquiv.map_add]
rfl
map_smul' := by
intro c v
ext i j
dsimp only []
rw [e.toMatrix_apply, Pi.smul_apply, LinearEquiv.map_smul]
rfl
invFun m j := ∑ i, m i j • e i
left_inv := by
intro v
ext j
exact e.sum_toMatrix_smul_self v j
right_inv := by
intro m
ext k l
simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply, LinearEquiv.apply_symm_apply]
