Linear Algebra - Trace

2026-09-06 · 随笔 · 43a908c205b5

迹(trace)是方阵对角线元素之和。它看起来是最简单的矩阵不变量,却是连接“矩阵”和“线性映射”两种视角的桥。这篇按 Mathlib 的组织方式过一遍:定义、基本性质、核心定理 $\operatorname{tr}(AB)=\operatorname{tr}(BA)$ 的完整推导、由它派生出的相似不变性,最后是与特征值的关系。所有定理名都对照 Mathlib/LinearAlgebra/Matrix/Trace.lean。

定义

Mathlib 里它就是一个普通函数,输入 $n\times n$ 矩阵,输出一个标量:

def Matrix.trace (A : Matrix n n R) : R :=
  ∑ i, diag A i

diag A i 就是 $A_{ii}$。要求 n 是有限类型(Fintype n),R 是加法交换幺半群(AddCommMonoid R),因为只用到了“有限个数相加”。注意定义里没有乘法,所以迹在任何能做加法的地方都有定义,不需要环。

同一个函数还被打包成两种带结构的形式:

三者的 toFun 都是同一个 trace。后两个的意义是:当你需要把“迹是线性的”这个事实交给别的定理(比如 map_sum)时,直接用打包好的版本,不用每次手证。

基本性质

全部是定义加求和的性质,不涉及矩阵乘法:

trace_one 值得看一眼:结果是 Fintype.card n,也就是维数,类型是自然数被强制转换到 R。

配套练习:$(AB)_{ij}$ 的下标怎么读,后面每一步推导都建立在那个读法上。

核心定理:$\operatorname{tr}(AB)=\operatorname{tr}(BA)$

手算

设 $A$ 是 $m\times n$,$B$ 是 $n\times m$。$AB$ 是 $m\times m$,$BA$ 是 $n\times n$,两个方阵大小不同,但迹相等:

两式被加项 $A_{ik}B_{ki}$ 与 $B_{ki}A_{ik}$ 差一个标量交换(mul_comm),两层求和的顺序差一个换序(Finset.sum_comm)。就这两步。

Mathlib 怎么拆

Mathlib 没有一步到位,而是拆成两个定理,恰好把 Finset.sum_comm 和 mul_comm 的分工分开了。

第一步,不需要交换律:

theorem trace_transpose_mul [AddCommMonoid R] [Mul R]
    (A : Matrix m n R) (B : Matrix n m R) :
    trace (Aᵀ * Bᵀ) = trace (A * B) :=
  Finset.sum_comm

证明就是 Finset.sum_comm 本身。展开看为什么:

第二行只是把 $\operatorname{tr}(AB)$ 的求和变量改名($i\leftrightarrow k$)。两边被加项逐字相同,是 $A_{ki}B_{ik}$,顺序都没换,只差外层求 $i$ 还是求 $k$。所以这一步只用 Finset.sum_comm,标量不需要能交换,类型类假设只有 [Mul R]。

第二步,才用到交换律:

theorem trace_mul_comm [AddCommMonoid R] [CommMagma R]
    (A : Matrix m n R) (B : Matrix n m R) :
    trace (A * B) = trace (B * A) := by
  rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]

三次改写:

1. ← trace_transpose:$\operatorname{tr}(AB)=\operatorname{tr}\big((AB)^{\mathsf T}\big)$
2. ← trace_transpose_mul:$\operatorname{tr}\big((AB)^{\mathsf T}\big)$,把它看成 $\operatorname{tr}(X^{\mathsf T}Y^{\mathsf T})$ 的形式后倒推回 $\operatorname{tr}(XY)$。需要先把 $(AB)^{\mathsf T}$ 写成两个转置的乘积
3. transpose_mul:$(AB)^{\mathsf T}=B^{\mathsf T}A^{\mathsf T}$

mul_comm 就藏在第 3 步。$(AB)^{\mathsf T}_{ij}=(AB)_{ji}=\sum_k A_{jk}B_{ki}$,而 $(B^{\mathsf T}A^{\mathsf T})_{ij}=\sum_k B_{ki}A_{jk}$,要让 $A_{jk}B_{ki}=B_{ki}A_{jk}$ 必须交换标量。所以 trace_mul_comm 的假设是 [CommMagma R],比上一步多了交换性。

这个拆法回答了“什么时候 $AB$ 可以调换”:

• 单独的 Finset.sum_comm 只能换求和号,得到的是 $\operatorname{tr}(A^{\mathsf T}B^{\mathsf T})=\operatorname{tr}(AB)$,$A$ 和 $B$ 的位置没动
• 要让 $A$、$B$ 真正换位,必须把 mul_comm 引进来,而它只作用在标量分量上
• 换位后的 $BA$ 与 $AB$ 仍是不同的矩阵(甚至大小不同),相等的只是迹这个标量

推论

循环不变,而非任意置换不变

theorem trace_mul_cycle (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
    trace (A * B * C) = trace (C * A * B) := by
  rw [trace_mul_comm, Matrix.mul_assoc]

$\operatorname{tr}(ABC)=\operatorname{tr}(CAB)=\operatorname{tr}(BCA)$,把 $(AB)$ 看成一个整体套 trace_mul_comm,再用结合律。但 $\operatorname{tr}(ABC)\ne\operatorname{tr}(ACB)$,一般情况下不成立。三个矩阵有 6 种排列,只有 3 种循环排列的迹相等。

相似不变

theorem trace_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    trace (↑M * N * ↑M⁻¹) = trace N

$\operatorname{tr}(PNP^{-1})=\operatorname{tr}(P^{-1}PN)=\operatorname{tr}(N)$,trace_mul_cycle 的直接应用。这条是迹能脱离矩阵、成为线性映射自身性质的原因:换一组基,矩阵变成 $PNP^{-1}$,迹不变。

Mathlib 据此定义了与基无关的 LinearMap.trace,并证明它与任何一组基下的矩阵迹一致:

theorem LinearMap.trace_eq_matrix_trace (f : M →ₗ[R] M) :
    trace R M f = Matrix.trace (LinearMap.toMatrix b b f)

外积的迹是内积

theorem trace_vecMulVec (a b : n → R) :
    trace (vecMulVec a b) = a ⬝ᵥ b

$\operatorname{tr}(uv^{\mathsf T})=\sum_i u_iv_i=u\cdot v$。推广一步:$\operatorname{tr}(A^{\mathsf T}B)=\sum_{i,j}A_{ij}B_{ij}$,这就是 Frobenius 内积,机器学习里 $\|A\|_F^2=\operatorname{tr}(A^{\mathsf T}A)$ 的来源。

与特征值的关系

迹是特征多项式次高项系数的相反数:

theorem trace_eq_neg_charpoly_coeff [Nonempty n] (M : Matrix n n R) :
    trace M = -M.charpoly.coeff (Fintype.card n - 1)

当特征多项式能完全分裂(比如域代数封闭)时,迹等于所有特征值之和(按重数计):

theorem trace_eq_sum_roots_charpoly [IsAlgClosed K] :
    A.trace = (Matrix.charpoly A).roots.sum

注意假设。实数域上 $\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ 没有实特征值,但迹是 0,所以“迹等于特征值之和”要么在复数域上说,要么加上 Splits 假设。定理名后缀 _of_splits 的版本就是带这个假设的。

迹不是什么

• $\operatorname{tr}(AB)\ne\operatorname{tr}(A)\operatorname{tr}(B)$。迹对加法是同态,对乘法不是。
• $\operatorname{tr}(ABC)\ne\operatorname{tr}(ACB)$。只有循环置换保迹。
• $\operatorname{tr}(AB)=\operatorname{tr}(BA)$ 不意味着 $AB=BA$。相等的是两个标量,矩阵本身连大小都可以不同。

层级速查