1.5 三维线性变换 · 从直觉到证明

一步一步建立直观

先预测，再点“演示本步”核对右图。每一步都重设到指定情形，随后可以自由修改参数。

旋转观察视角，留意箭头在屏幕上变短并不意味着空间长度变小。屏幕只是三维对象的投影，下面的长度读数才使用三维坐标计算。操作参数改变数学对象，拖动空白处改变相机，这两件事必须明确区分。

绕 $z$ 轴转四分之一圈时， $(x,y,z)$ 变为 $(-y,x,z)$ 。横纵分量互换并改变一个符号，高度保持。平方长度仍是 $x^2+y^2+z^2$ ，因此图像中的转动有一条可以独立核对的代数不变量。可以在任意角度先记录长度，再修改转角复核这个守恒关系。

切换到投影模式，垂直虚线显示被丢弃的高度。所有只在 $z$ 坐标上不同的点都有同一个平面像。旋转保留恢复原状态的信息，投影则一般做不到；能否求逆取决于这个信息差别，而不是画面是否仍有三维感。

二维的两个基向量变成三维的三个。想象透明方盒从同一角出发的三条棱，分别代表 $e_1,e_2,e_3$ 。线性变换把盒子变成平行六面体；记录三条棱的新方向，内部每点的位置就由同样的线性组合决定。九个矩阵元素依旧只是三份目的地记录。

绕竖直轴旋转四分之一圈时，横向箭头变为纵向，纵向箭头变为负横向，竖直箭头保持不动。把这三条记录排成列，旋转矩阵便自然出现。应用于 $(2,1,3)$ 时，组合三根新基箭头即可得到 $(-1,2,3)$ 。

如何检查公式真像旋转？可以计算平方长度。变换后是 $(-y)^2+x^2+z^2$ ，恰等于原来的 $x^2+y^2+z^2$ 。一次数值算例不能证明一般结论，所以应保留任意的 $x,y,z$ 。Lean 在这里验证的就是这个一般恒等式。

三维还有一个新现象：不同轴的旋转通常不交换。拿一本书，先绕竖直方向再绕左右方向转动，随后试着倒过来做，会得到不同姿态。不能把二维平面内旋转的交换性推广到所有三维旋转。

本节不要求先掌握一整套旋转参数，只需学会从列读动作。后面遇到体积，回想这个盒子；遇到核，想象它压成面或线；遇到特征向量，寻找变换后仍留在原直线上的方向。三维只是多了一根基，核心推理仍是同一套。

与本图相连的定义与证明：1.10 · 叉积与两个输入都垂直。本节的具体条件与形式化范围见下文。

三维矩阵有三列，分别记录三个基向量去向。二维的“面积”将在三维变成“体积”。

绕 $z$ 轴逆时针旋转 $90^\circ$ 的矩阵为 $R=\begin{bmatrix}0&-1&0\\1&0&0\\0&0&1\end{bmatrix},\quad R(x,y,z)=(-y,x,z).$

例 1.5.1 把概念用于具体计算

$(2,1,3)$ 变为 $(-1,2,3)$ 。两者平方长度均为 $14$ ，且 $z$ 坐标保持不变；连续作用四次回到原向量。

对 $(1,0,0)$ 连续作用两次 $R$ 。

展开解答与检查

答案 $(-1,0,0)$ ，不是原向量。

Lean 对照 1.5.1 命题、证明与适用边界

验证该 $90^\circ$ 旋转保持平方长度。未宣称已经证明一般三维旋转的分类。

LinearAlgebra.rotation_preserves_square_norm

theorem rotation_preserves_square_norm (x y z : ℝ) :
    (-y)^2 + x^2 + z^2 = x^2 + y^2 + z^2 := by ring

原课对照观课问题、视频与图示

观察三根基向量如何确定三维动作，并检查旋转时长度是否保持。

点击后连接 YouTube；播放器不可用时可通过上方原链接观看。