1.3 线性变换与矩阵

1.3.1 用两个箭头描述整个平面的运动¶

设想写一个程序，让平面上的每个点移动。逐点列出目的地不现实，我们需要压缩信息的规则。线性规则承诺：一个向量若由两个向量按一定比例拼成，变换后仍按同样比例拼成。知道基向量的去向，就能恢复所有点的去向。

任意输入都能拆为 $xe_1+ye_2$。假如 $e_1$ 被送到 $(2,0)$，$e_2$ 被送到 $(1,3)$，只需取 $x$ 份第一根新箭头与 $y$ 份第二根新箭头，结果就是 $(2x+y,3y)$。矩阵把两条目的地记录并排存放，所以它们是列，而不是行。

1.3.2 公式从基向量的去向长出来¶

取 $x=1,y=2$，画一份 $(2,0)$ 和两份 $(1,3)$，终点为 $(4,6)$。再按坐标计算，会发现每一行都在计算输出的一个分量。列的解释告诉我们动作是什么，行的解释告诉我们输出数字怎么计算。

打开矩阵实验，先只改变一列。预测哪根基箭头会动、哪些输入受影响，再播放从单位网格到目标网格的变化。中间的连续变形只是展示方式；数学对象是指定的输入输出关系，不能把动画经过的每个阶段都当成同一个变换。

最后检查边界：平移虽然规整，却把零向量送到非零位置，因此不线性。只看水平线与竖直线是否笔直也不够，仍需检查任意向量的相加与缩放。下面的 Lean 命题精确表达的就是这个承诺，而不是对一张网格图作判断。

theorem linear_combination {V W : Type*} [AddCommGroup V] [Module ℝ V]
    [AddCommGroup W] [Module ℝ W] (T : V →ₗ[ℝ] W) (a b : ℝ) (u v : V) :
    T (a • u + b • v) = a • T u + b • T v := by simp