English
Restricting scalars commutes with taking the matrix representation of a basis: the matrix of the restricted basis equals the matrix of the original basis with entries restricted to the subfield.
Русский
Ограничение скаляров commuting с матричным представлением базиса: матрица ограниченного базиса равна матрице исходного базиса с соответствующим ограничением коэффициентов.
LaTeX
$$$ (\mathrm{algebraMap}_{R_2 \to S}).mapMatrix\bigl((b.\restrictScalars R_2).toMatrix v\bigr) = b.toMatrix\bigl(\lambda i \, \mapsto (v i).val\bigr)$$$
Lean4
theorem restrictScalars_toMatrix [Fintype ι] [DecidableEq ι] {S : Type*} [CommRing S] [Nontrivial S] [Algebra R₂ S]
[Module S M₂] [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S] (b : Basis ι S M₂) (v : ι → span R₂ (Set.range b)) :
(algebraMap R₂ S).mapMatrix ((b.restrictScalars R₂).toMatrix v) = b.toMatrix (fun i ↦ (v i : M₂)) :=
by
ext
rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Basis.restrictScalars_repr_apply,
Basis.toMatrix_apply]
