English
The trace matrix under a matrix-multiplication action equals P^T · Tr(b) · P.
Русский
Матрица следа после умножения матрицы на вектор эквивалентна P^T · Tr(b) · P.
LaTeX
$$$\\operatorname{traceMatrix}_A((P.map(\\mathrm{algebraMap}\\,A\,B)) \\cdot^{\\mathrm{vec}}\, b) = P^{T} \\cdot \\operatorname{traceMatrix}_A(b) \\cdot P$$$
Lean4
theorem traceMatrix_of_matrix_vecMul [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
traceMatrix A (b ᵥ* P.map (algebraMap A B)) = Pᵀ * traceMatrix A b * P :=
by
ext (α β)
rw [traceMatrix_apply, vecMul, dotProduct, vecMul, dotProduct, Matrix.mul_apply, BilinForm.sum_left,
Fintype.sum_congr _ _ fun i : κ =>
BilinForm.sum_right _ _ (b i * P.map (algebraMap A B) i α) fun y : κ => b y * P.map (algebraMap A B) y β,
sum_comm]
congr; ext x
rw [Matrix.mul_apply, sum_mul]
congr; ext y
rw [map_apply, traceForm_apply, mul_comm (b y), ← smul_def]
simp only [id.smul_eq_mul, RingHom.id_apply, map_apply, transpose_apply, LinearMap.map_smulₛₗ, Algebra.smul_mul_assoc]
rw [mul_comm (b x), ← smul_def]
ring_nf
rw [mul_assoc]
simp [mul_comm]
