English
If M1,M2 are R-modules with bases b1 and b2 indexed by finite sets ι1 and ι2, then the standard basis of the space of R-linear maps M1 → M2 is indexed by ι2 × ι1. The basis element corresponding to (i, j) sends the j-th basis vector of M1 to the i-th basis vector of M2 and all other basis vectors to 0.
Русский
Если M1 и M2 — модули над R с базисами b1 и b2, индексируемыми конечными множествоами ι1 и ι2, то стандартная база пространства отображений M1 → M2 имеет индексы в ι2 × ι1: элемент (i, j) посылает b1_j в b2_i, а все прочие базисные вектора в 0.
LaTeX
$$$\\text{Basis}_{ι_2 \\times ι_1}(M_1 \\to_R M_2) \\quad\\text{where}\\quad L_{i,j}(b_1(j)) = b_2(i),\\; L_{i,j}(b_1(k))=0\\ (k\\neq j)$$$
Lean4
/-- The standard basis of the space linear maps between two modules
induced by a basis of the domain and codomain.
If `M₁` and `M₂` are modules with basis `b₁` and `b₂` respectively indexed
by finite types `ι₁` and `ι₂`,
then `Basis.linearMap b₁ b₂` is the basis of `M₁ →ₗ[R] M₂` indexed by `ι₂ × ι₁`
where `(i, j)` indexes the linear map that sends `b j` to `b i`
and sends all other basis vectors to `0`. -/
@[simps! -isSimp repr_apply repr_symm_apply]
noncomputable def linearMap (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : Basis (ι₂ × ι₁) R (M₁ →ₗ[R] M₂) :=
(Matrix.stdBasis R ι₂ ι₁).map (LinearMap.toMatrix b₁ b₂).symm
