English
For a bilinear map B and linear maps l, r, the matrix of the composed operation B.compl₁₂ l r with respect to bases b1', b2' equals the product of the matrices representing l, B, and r, with a transpose on the left factor.
Русский
Для билинейного отображения B и линейных отображений l, r матрица составной операции B.compl₁₂ l r по основаниям b1', b2' равна произведению матриц, соответствующих l, B и r, при чём левая часть транспонируется.
LaTeX
$$$$ \\mathrm{toMatrix}_2^{b_1',b_2'}\\bigl(B\\!:\\!\\mathrm{compl}_{12}\\,l\,r\\bigr) = \\bigl(\\mathrm{toMatrix}_{b_1',b_1} l\\bigr)^{\\top} \\; \\mathrm{toMatrix}_2^{b_1,b_2}(B) \\; \\bigl(\\mathrm{toMatrix}_{b_2',b_2} r\\bigr). $$$$
Lean4
theorem toMatrix₂_compl₁₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁) (r : M₂' →ₗ[R] M₂) :
LinearMap.toMatrix₂ b₁' b₂' (B.compl₁₂ l r) =
(toMatrix b₁' b₁ l)ᵀ * LinearMap.toMatrix₂ b₁ b₂ B * toMatrix b₂' b₂ r :=
by
ext i j
simp only [LinearMap.toMatrix₂_apply, compl₁₂_apply, transpose_apply, Matrix.mul_apply, LinearMap.toMatrix_apply,
sum_mul]
rw [sum_comm]
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul b₁ b₂]
rw [Finsupp.sum_fintype]
· apply sum_congr rfl
rintro i' -
rw [Finsupp.sum_fintype]
· apply sum_congr rfl
rintro j' -
simp only [smul_eq_mul, mul_assoc, mul_comm, mul_left_comm]
· intros
simp only [zero_smul, smul_zero]
· intros
simp only [zero_smul, Finsupp.sum_zero]
