Lean 学习笔记——7. 线性代数基础

Some content in this article was created with AI assistance. Please verify as needed.

mathlib 区分坐标函数、线性映射和矩阵。三者都能描述线性变换，但保存的数据和可直接使用的定理不同；选定基以后，才谈得上用矩阵表示抽象线性映射。

import Mathlib

open Matrix
open scoped BigOperators

本篇只讨论有限维实向量、矩阵、线性映射和子空间，集中说明这些对象的类型、转换方式和常用证明入口。

有限向量

向量表示

长度为 n、元素类型为 α 的坐标向量可以直接表示成：

Fin n → α

Fin n 是小于 n 的自然数类型。函数的定义域决定向量长度，因此不同长度的向量具有不同类型。

#check (fun i : Fin 3 => (i : Nat))
#check (0 : Fin 3)
#check (2 : Fin 3)

这种表示与普通数组不同。Array α 的长度是运行时数据，Fin n → α 的维数则出现在类型中。需要固定维数的数学证明通常使用后者。

向量字面量

mathlib 提供 ![...] 记号构造短向量：

def u : Fin 2 → ℝ := ![3, 4]
def v : Fin 2 → ℝ := ![1, -2]

example : u 0 = 3 := by
  rfl

example : u 1 = 4 := by
  rfl

下标 0 会根据上下文推断为 Fin 2。若写出越界下标，Lean 会在 elaboration 阶段拒绝代码，而不是等到运行时抛出异常。

向量加法和数乘来自函数类型上的逐点实例：

example : u + v = ![4, 2] := by
  funext i
  fin_cases i <;> norm_num [u, v]

example : (2 : ℝ) • u = ![6, 8] := by
  funext i
  fin_cases i <;> norm_num [u]

数乘符号 • 用 \smul 输入，等价的命名写法是 SMul.smul。命名形式揭示了运算来自类型类实例，但在线性代数公式中，a • x 通常比 SMul.smul a x 更容易读。

这里 funext i 把函数相等转成逐点相等，fin_cases i 枚举 Fin 2 的两个可能值。<;> 表示把后面的 tactic 应用于前一个 tactic 产生的所有目标。

向量外延

两个向量相等，当且仅当每个坐标都相等。可以直接使用 funext：

example (x y : Fin 3 → ℝ)
    (h : ∀ i, x i = y i) : x = y := by
  funext i
  exact h i

这不是线性代数专用定理，而是函数外延。因为坐标向量本来就是函数，所以普通函数 API 可以直接使用。

点积

有限向量的点积是逐坐标乘积之和：

example : dotProduct u v = -5 := by
  norm_num [dotProduct, u, v]

展开定义后，目标是 Fin 2 上的有限求和。小维数计算可以交给 norm_num；一般维数的证明则应使用 dotProduct_add、dotProduct_comm 等接口，而不是反复展开求和。

example (x y z : Fin 3 → ℝ) :
    dotProduct x (y + z) = dotProduct x y + dotProduct x z := by
  exact dotProduct_add x y z

矩阵

矩阵表示

mathlib 中的矩阵本质上是二元函数：

Matrix m n α = m → n → α

m 是行指标类型，n 是列指标类型。一个 $2\times 3$ 实矩阵可以写成：

def A : Matrix (Fin 2) (Fin 3) ℝ :=
  !![1, 2, 3;
     4, 5, 6]

example : A 0 2 = 3 := by
  rfl

example : A 1 0 = 4 := by
  rfl

矩阵采用两个下标，因此 A i j 就是第 i 行、第 j 列的元素。行列指标不必是自然数区间；使用 Fin n 只是有限维计算中最常见的选择。

矩阵外延

矩阵也是函数，所以相等性仍然通过逐项证明：

example {m n : Type} (B C : Matrix m n ℝ)
    (h : ∀ i j, B i j = C i j) : B = C := by
  ext i j
  exact h i j

ext i j 在这里连续应用函数外延。证明具体小矩阵相等时，可以再枚举行列下标：

example : A + A =
    !![2, 4, 6;
       8, 10, 12] := by
  ext i j
  fin_cases i <;> fin_cases j <;> norm_num [A]

单位矩阵

单位矩阵由相等判断定义：对角线上为 1，其余位置为 0。

example : (1 : Matrix (Fin 2) (Fin 2) ℝ) =
    !![1, 0;
       0, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp

矩阵的 1 来自方阵上的幺元实例。它不是所有矩阵类型都有的值：行指标和列指标必须相同，矩阵乘法的尺寸才闭合。

矩阵乘向量

矩阵乘向量记号 A *ᵥ x 对应 Matrix.mulVec A x。这类组合记号不必死记输入缩写：将鼠标悬停在 *ᵥ 上即可查看当前 Lean 扩展提供的输入方式，也可以在命令面板中按 mulVec 或符号搜索。

mulVec 表示矩阵乘列向量：

def B : Matrix (Fin 2) (Fin 2) ℝ :=
  !![2, 1;
     0, 3]

example : B *ᵥ u = ![10, 12] := by
  funext i
  fin_cases i <;> norm_num [B, u, Matrix.mulVec, dotProduct]

类型已经记录尺寸：

B : Matrix (Fin 2) (Fin 2) ℝ
u : Fin 2 → ℝ
B *ᵥ u : Fin 2 → ℝ

如果矩阵列指标与向量指标不同，表达式无法通过类型检查。这对应普通数值库中的 shape 检查，但发生在运行前。

矩阵乘法

矩阵乘法对中间指标求和：

example : B * (1 : Matrix (Fin 2) (Fin 2) ℝ) = B := by
  simp

example : (1 : Matrix (Fin 2) (Fin 2) ℝ) * B = B := by
  simp

结合律需要中间指标有限，并要求系数具有足够的半环结构：

example {l m n p : Type}
    [Fintype m] [Fintype n]
    [DecidableEq m] [DecidableEq n]
    (X : Matrix l m ℝ) (Y : Matrix m n ℝ)
    (Z : Matrix n p ℝ) :
    (X * Y) * Z = X * (Y * Z) := by
  exact Matrix.mul_assoc X Y Z

证明一般矩阵恒等式时应优先使用矩阵 API。只有固定的 $2\times2$ 或 $3\times3$ 数值计算才适合枚举下标。

线性映射

普通函数与线性映射

普通函数类型没有记录保持加法和数乘的性质：

V → W

线性映射则写成：

V →ₗ[𝕜] W

它包含函数和两项证明：保持加法、保持标量乘法。若把标量类型改名为 K，完全展开的 ASCII 类型是 LinearMap K V W。→ₗ 是 mathlib 的专用 notation，阅读时应把它理解为“带标量环参数的线性映射类型”。

section

variable {𝕜 V W : Type}
variable [Semiring 𝕜]
variable [AddCommMonoid V] [Module 𝕜 V]
variable [AddCommMonoid W] [Module 𝕜 W]
variable (f : V →ₗ[𝕜] W)

#check f.toFun
#check f.map_add
#check f.map_smul

end

结构被打包以后，定律不需要在每个定理中重新作为前提传入。

构造线性映射

二维向量的坐标交换是一个线性映射：

def swapLinear : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) where
  toFun x := ![x 1, x 0]
  map_add' x y := by
    funext i
    fin_cases i <;> simp
  map_smul' c x := by
    funext i
    fin_cases i <;> simp

字段名末尾的 ' 表示这是构造结构时需要填写的证明字段。构造完成后，对外通常使用无撇号的定理 swapLinear.map_add 和 swapLinear.map_smul。

example : swapLinear u = ![4, 3] := by
  rfl

example (x y : Fin 2 → ℝ) :
    swapLinear (x + y) = swapLinear x + swapLinear y := by
  exact swapLinear.map_add x y

线性映射提供 CoeFun 实例，因此可以直接写 swapLinear u，但它仍然不是裸函数；保持线性的证明仍保存在结构中。

线性映射外延

两个线性映射逐点相等即可证明结构相等：

example {𝕜 V W : Type}
    [Semiring 𝕜]
    [AddCommMonoid V] [Module 𝕜 V]
    [AddCommMonoid W] [Module 𝕜 W]
    (f g : V →ₗ[𝕜] W)
    (h : ∀ x, f x = g x) : f = g := by
  ext x
  exact h x

无需分别比较 toFun、map_add' 和 map_smul'。证明字段具有 proof irrelevance，外延定理只要求比较真正影响行为的函数值。

恒等与复合

线性映射的复合仍是线性映射：

example : swapLinear.comp swapLinear = LinearMap.id := by
  ext x i
  fin_cases i <;> rfl

swapLinear.comp swapLinear 在类型层面已经携带复合后的线性证明。上面的证明只需检查复合函数确实逐点等于恒等函数。

这个证明依次经过四层：

1. 用线性映射 API 组织对象；
2. 用 ext 把结构相等降为函数值相等；
3. 用 fin_cases 处理固定维数；
4. 最后用 rfl、simp 或 norm_num 完成坐标计算。

子空间

Submodule

Submodule 𝕜 V 表示对零、加法和标量乘法封闭的向量集合。成员关系仍写成普通的 x ∈ U。

section

variable {𝕜 V : Type}
variable [Semiring 𝕜]
variable [AddCommMonoid V] [Module 𝕜 V]
variable (U W : Submodule 𝕜 V)

#check (⊥ : Submodule 𝕜 V)
#check (⊤ : Submodule 𝕜 V)
#check U ⊓ W
#check U ⊔ W

example : U ⊓ W ≤ U := by
  exact inf_le_left

end

⊥ 是只含零向量的子空间，⊤ 是整个空间，⊓ 是交，⊔ 是包含两个子空间的最小子空间。这里使用的是一般格结构，而不是四个互不相关的专用函数。

坐标泛函

取二维向量的第二个坐标会得到一个线性泛函：

def secondCoord : (Fin 2 → ℝ) →ₗ[ℝ] ℝ where
  toFun x := x 1
  map_add' x y := by
    rfl
  map_smul' c x := by
    rfl

它的核就是横轴：

def xAxis : Submodule ℝ (Fin 2 → ℝ) :=
  LinearMap.ker secondCoord

example (x : Fin 2 → ℝ) : x ∈ xAxis ↔ x 1 = 0 := by
  rfl

example : ![(3 : ℝ), 0] ∈ xAxis := by
  rfl

example : ![(3 : ℝ), 1] ∉ xAxis := by
  norm_num [xAxis, secondCoord]

这个例子把三个概念连在一起：线性方程由线性泛函表示，齐次方程的解集是该映射的核，而核天然具有子空间结构。

核与像

对任意线性映射 f : V →ₗ[𝕜] W：

#check LinearMap.ker
#check LinearMap.range

• f.ker : Submodule 𝕜 V；
• f.range : Submodule 𝕜 W。

成员关系分别对应：

x ∈ f.ker    ↔ f x = 0
y ∈ f.range  ↔ ∃ x, f x = y

核处理齐次方程，像处理方程是否有解。很多单射、满射结论都可以改写成关于核和像的子空间等式。

example : LinearMap.ker swapLinear = ⊥ := by
  ext x
  simp only [LinearMap.mem_ker, Submodule.mem_bot]
  constructor
  · intro hx
    funext i
    fin_cases i
    · simpa [swapLinear] using congrFun hx (1 : Fin 2)
    · simpa [swapLinear] using congrFun hx (0 : Fin 2)
  · rintro rfl
    exact swapLinear.map_zero

这个证明利用 swap ∘ swap = id 的事实说明 swap x = 0 只能推出 x = 0。apply_fun 把等式两边同时应用一个函数；当逆映射很明显时，这是证明单射的常用方法。

张成与基

span

给定向量集合 s : Set V，Submodule.span 𝕜 s 是包含 s 的最小子空间。

section

variable {𝕜 V : Type}
variable [Semiring 𝕜]
variable [AddCommMonoid V] [Module 𝕜 V]
variable (s : Set V) (x : V)

#check Submodule.span 𝕜 s

example (hx : x ∈ s) : x ∈ Submodule.span 𝕜 s := by
  exact Submodule.subset_span hx

end

不要把 span 理解成一个返回向量列表的算法。它首先是满足最小性条件的数学子空间；是否能计算出有限基是另一个问题。

线性无关与基

mathlib 分别使用：

#check LinearIndependent
#check Module.Basis
#check Module.finrank

LinearIndependent 𝕜 v 讨论向量族 v : ι → V 是否线性无关；Basis ι 𝕜 V 不只是一组向量，还携带它们给出的坐标同构。Module.finrank 𝕜 V 则给出有限维空间的维数。

这三者解决的问题不同：

对象	主要信息
LinearIndependent	线性组合表示是否唯一
span	一组向量能生成哪些向量
Basis	同时具有线性无关与生成性，并提供坐标
finrank	有限维空间的维数

换基、秩、行列式和特征值依赖更多有限维类型类与基的 API，本篇不展开这些主题。

证明层次

坐标证明

固定低维数值问题适合直接计算：

example : B *ᵥ ![(2 : ℝ), 5] = ![9, 15] := by
  funext i
  fin_cases i <;> norm_num [B, Matrix.mulVec, dotProduct]

这类证明清楚、可执行，但只适用于当前维数和具体矩阵。

结构证明

一般维数下应使用结构定理：

example {𝕜 V W : Type}
    [Semiring 𝕜]
    [AddCommMonoid V] [Module 𝕜 V]
    [AddCommMonoid W] [Module 𝕜 W]
    (f : V →ₗ[𝕜] W) : f 0 = 0 := by
  exact f.map_zero

结构证明不依赖坐标和维数。若结论只使用线性映射公理，把类型写死成二维实向量反而会丢失复用性。

选择抽象层

可以按问题选择表示：

问题	合适对象
固定维数的数值计算	Fin n → ℝ、Matrix
保持加法和数乘的变换	LinearMap
齐次方程的解集	LinearMap.ker
可达向量集合	LinearMap.range
封闭的向量集合	Submodule
生成空间	Submodule.span
坐标系与换基	Basis

固定坐标计算使用矩阵，映射复合使用 LinearMap，解集和封闭性使用 Submodule。若一个证明反复展开坐标或重新证明线性，通常说明对象选得过低；换到带结构的类型后，可以直接调用相应定理。