9. 线性代数

9.1. 向量空间与线性映射

9.1.1. 向量空间

我们将直接从抽象线性代数开始，讨论定义在任意域上的向量空间。不过，你也可以在 Section 9.4.1 中找到关于矩阵的信息，该部分在逻辑上并不依赖于本抽象理论。Mathlib 实际上处理的是更广义的线性代数，使用模（module）一词，但现在我们暂时当作这只是一个古怪的拼写习惯。

“设 \(K\) 是一个域，且 \(V\) 是定义在 \(K\) 上的向量空间”（并将其作为后续结论的隐式参数）的表达方式是：

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

我们在 Chapter 7 中解释了为什么需要两个独立的类型类 [AddCommGroup V] 和 [Module K V]。

简而言之，数学上我们想表达的是：拥有一个域 \(K\) 上的向量空间结构意味着拥有一个加法交换群结构。虽然可以告诉 Lean 这一点，但如果这样做，每当 Lean 需要在类型 \(V\) 上寻找该群结构时，它就会尝试去寻找带有完全未指定域 \(K\) 的向量空间结构，而这个 \(K\) 无法从 \(V\) 中推断出来。这会严重影响类型类合成系统的效率和稳定性。

向量 v 与标量 a 的乘法记作 a • v。下面示例列举了该操作与加法之间的若干代数规则。当然，simp 或 apply? 策略可以自动找到这些证明。还有一个 module 策略，类似于在交换环中使用 ring 策略、在群中使用 group 策略，可以根据向量空间和域的公理自动解决相关目标。但需要记住的是，在引理名称中，标量乘法通常缩写为 smul。

example (a : K) (u v : V) : a • (u + v) = a • u + a • v :=
  smul_add a u v

example (a b : K) (u : V) : (a + b) • u = a • u + b • u :=
  add_smul a b u

example (a b : K) (u : V) : a • b • u = b • a • u :=
  smul_comm a b u

作为对更高级读者的简要提示，正如术语所暗示的那样，Mathlib 的线性代数不仅涵盖了定义在（不一定是交换）环上的模（modules）。事实上，它甚至涵盖了半环上的半模（semi-modules）。如果你认为不需要如此广泛的泛化，可以思考下面这个例子，它很好地体现了理想对子模作用的许多代数规则：

example {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Module (Ideal R) (Submodule R M) :=
  inferInstance

9.1.2. 线性映射

接下来我们需要引入线性映射。类似于群同态，Mathlib 中的线性映射是“打包”的映射，即由一个映射和其线性性质证明组成的整体。这些打包映射在应用时会自动转换为普通函数。关于这一设计的更多信息，请参见 Chapter 7。

两个域 K 上的向量空间 V 和 W 之间的线性映射类型记作 V →ₗ[K] W ，其中下标的 l 表示“linear”（线性）。一开始在符号中显式指定 K 可能感觉有些奇怪，但当涉及多个域时，这一点尤为重要。例如，从复数域 \(ℂ\) 到 \(ℂ\) 的实线性映射形式为 \(z ↦ az + b\bar{z}\) ，而复线性映射则仅限于形式为 \(z ↦ az\) 的映射，这一区别在复分析中极为关键。

variable {W : Type*} [AddCommGroup W] [Module K W]

variable (φ : V →ₗ[K] W)

example (a : K) (v : V) : φ (a • v) = a • φ v :=
  map_smul φ a v

example (v w : V) : φ (v + w) = φ v + φ w :=
  map_add φ v w

注意，V →ₗ[K] W 本身也携带了丰富的代数结构（这也是将这些映射打包的动机之一）。它是一个 K-向量空间，因此我们可以对线性映射进行加法运算，也可以对它们进行标量乘法。

variable (ψ : V →ₗ[K] W)

#check (2 • φ + ψ : V →ₗ[K] W)

使用打包映射的一个缺点是，无法直接使用普通函数的组合运算。我们需要使用专门的组合函数 LinearMap.comp，或者使用专用符号 ∘ₗ 来表示线性映射的组合。

variable (θ : W →ₗ[K] V)

#check (φ.comp θ : W →ₗ[K] W)
#check (φ ∘ₗ θ : W →ₗ[K] W)

构造线性映射主要有两种方式。第一种是通过提供函数本体和线性性质的证明来构建该结构。通常，可以借助代码操作快速完成：你只需输入 example : V →ₗ[K] V := _ 然后对下划线使用“生成骨架”（Generate a skeleton）代码操作，即可自动生成所需的结构框架。

example : V →ₗ[K] V where
  toFun v := 3 • v
  map_add' _ _ := smul_add ..
  map_smul' _ _ := smul_comm ..

你可能会好奇为什么 LinearMap 结构中用于证明的字段名称都带有撇号。这是因为这些证明是在函数强制转换（coercion）之前定义的，因此它们是基于 LinearMap.toFun 表达的。随后，它们又被重新表达为基于函数强制转换的 LinearMap.map_add 和 LinearMap.map_smul。事情还没结束。我们还需要一个适用于任意保持加法的（打包）映射的 map_add 版本，比如加法群同态、线性映射、连续线性映射、K-代数映射等。这个版本是定义在根命名空间的 map_add。而中间版本 LinearMap.map_add 虽有些冗余，但支持点记法（dot notation），在某些情况下使用起来更方便。map_smul 也有类似情况。整体框架请参见 Chapter 7 的详细解释。

#check (φ.map_add' : ∀ x y : V, φ.toFun (x + y) = φ.toFun x + φ.toFun y)
#check (φ.map_add : ∀ x y : V, φ (x + y) = φ x + φ y)
#check (map_add φ : ∀ x y : V, φ (x + y) = φ x + φ y)

我们也可以利用 Mathlib 中已有的线性映射，通过各种组合子（combinators）来构造新的线性映射。例如，上述例子已经在 Mathlib 中以 LinearMap.lsmul K V 3 的形式存在。这里 K 和 V 是显式参数，原因有几个：最主要的是，如果只写 LinearMap.lsmul 3，Lean 无法推断出 V，甚至无法推断出 K。此外，LinearMap.lsmul K V 本身也是一个有趣的对象：它的类型是 K →ₗ[K] V →ₗ[K] V ，意味着它是一个从域 K`（视为其自身上的向量空间）到从 `V 到 V 的 K-线性映射空间的线性映射。

#check (LinearMap.lsmul K V 3 : V →ₗ[K] V)
#check (LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V)

还有一个线性同构类型 LinearEquiv，用符号表示为 V ≃ₗ[K] W ，对于 f : V ≃ₗ[K] W，它的逆映射是 f.symm : W ≃ₗ[K] V 。两个线性同构 f 和 g 的复合是 f.trans g ，也可用符号 f ≪≫ₗ g 表示。V 的恒等同构是 LinearEquiv.refl K V ，该类型的元素在需要时会自动强制转换为对应的同态映射或函数。

example (f : V ≃ₗ[K] W) : f ≪≫ₗ f.symm = LinearEquiv.refl K V :=
  f.self_trans_symm

可以使用 LinearEquiv.ofBijective 从一个双射的同态构造线性同构。这样构造的逆映射函数是不可计算的。

noncomputable example (f : V →ₗ[K] W) (h : Function.Bijective f) : V ≃ₗ[K] W :=
  .ofBijective f h

请注意，在上述例子中，Lean 利用声明的类型自动识别 .ofBijective 是指 LinearEquiv.ofBijective，无需显式打开命名空间。

9.1.3. 向量空间的直和与直积

我们可以利用已有的向量空间，通过直和和直积构造新的向量空间。从两个向量空间开始，在该情形下直和与直积无区别，我们可以直接使用积类型。下面的代码片段展示了如何将所有结构映射（含入（inclusion）映射和投影映射）构造为线性映射，以及构造映射到积空间和从和空间出的万有性质（universal properties）。如果你对范畴论中和与积的区别不熟悉，可以忽略“万有性质”相关术语，专注于示例中的类型即可。

section binary_product

variable {W : Type*} [AddCommGroup W] [Module K W]
variable {U : Type*} [AddCommGroup U] [Module K U]
variable {T : Type*} [AddCommGroup T] [Module K T]

-- 第一投影映射
example : V × W →ₗ[K] V := LinearMap.fst K V W

-- 第二投影映射
example : V × W →ₗ[K] W := LinearMap.snd K V W

-- 直积的万有性质
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : U →ₗ[K]  V × W := LinearMap.prod φ ψ

-- 直积映射满足预期行为，第一分量
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.fst K V W ∘ₗ LinearMap.prod φ ψ = φ := rfl

-- 直积映射满足预期行为，第二分量
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.snd K V W ∘ₗ LinearMap.prod φ ψ = ψ := rfl

-- 我们也可以并行组合映射
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) : (V × W) →ₗ[K] (U × T) := φ.prodMap ψ

-- 这只是通过将投影与万有性质结合实现
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) :
  φ.prodMap ψ = (φ ∘ₗ .fst K V W).prod (ψ ∘ₗ .snd K V W) := rfl

-- 第一包含（inclusion）映射
example : V →ₗ[K] V × W := LinearMap.inl K V W

-- 第二含入映射
example : W →ₗ[K] V × W := LinearMap.inr K V W

-- 直和（又称余积）的万有性质
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : V × W →ₗ[K] U := φ.coprod ψ

-- 余积映射满足预期行为，第一分量
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inl K V W = φ :=
  LinearMap.coprod_inl φ ψ

-- 余积映射满足预期行为，第二分量
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inr K V W = ψ :=
  LinearMap.coprod_inr φ ψ

-- 余积映射的定义符合预期
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) (v : V) (w : W) :
    φ.coprod ψ (v, w) = φ v + ψ w :=
  rfl

end binary_product

现在我们转向任意族向量空间的直和与直积。这里我们将展示如何定义一个向量空间族，并访问直和与直积的万有性质。请注意，直和符号限定在 DirectSum 命名空间中，且直和的万有性质要求索引类型具备可判定等价性（这在某种程度上是实现上的偶然情况）。

section families
open DirectSum

variable {ι : Type*} [DecidableEq ι]
         (V : ι → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]

-- 直和的万有性质将从各个直和因子映射出的映射组装成从直和映射出的映射
example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
  DirectSum.toModule K ι W φ

-- 直积的万有性质将映射到各个因子的映射组装成映射到直积
example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
  LinearMap.pi φ

-- 来自直积的投影映射
example (i : ι) : (Π j, V j) →ₗ[K] V i := LinearMap.proj i

-- 含入映射到直和
example (i : ι) : V i →ₗ[K] (⨁ i, V i) := DirectSum.lof K ι V i

-- 含入映射到直积
example (i : ι) : V i →ₗ[K] (Π i, V i) := LinearMap.single K V i

-- 若 `ι` 是有限类型，直和与直积之间存在线性同构
example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
  linearEquivFunOnFintype K ι V

end families

9.2. 子空间和商空间

9.2.1. 子空间

正如线性映射是打包结构，向量空间 V 的线性子空间同样是一个打包结构，包含 V 中的一个子集，称为子空间的载体（carrier），并具备相关的闭合性质。这里依然使用“模（module）”一词，而非向量空间，是因为 Mathlib 在线性代数中采用了更广泛的理论框架。

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (U : Submodule K V) {x y : V} (hx : x ∈ U) (hy : y ∈ U) :
    x + y ∈ U :=
  U.add_mem hx hy

example (U : Submodule K V) {x : V} (hx : x ∈ U) (a : K) :
    a • x ∈ U :=
  U.smul_mem a hx

在上述例子中，需要理解的是，Submodule K V 表示 V 上的 K-线性子空间的类型，而非 Set V 中元素 U 的谓词 IsSubmodule U。Submodule K V 配备了到 Set V 的强制类型转换（coercion）以及对 V 的成员关系谓词。有关该设计的原因及实现方式，可参见 Section 7.3。

当然，两个子空间相等当且仅当它们包含相同的元素。此性质已被注册用于 ext 策略，后者可用来证明两个子空间相等，方式与证明两个集合相等相同。

例如，要表述并证明实数域 ℝ 是复数域 ℂ 上的一个 ℝ-线性子空间，实质上是构造一个类型为 Submodule ℝ ℂ 的项，使其强制转换为 Set ℂ 后正是 ℝ，或者更准确地说，是 ℝ 在 ℂ 中的像。

noncomputable example : Submodule ℝ ℂ where
  carrier := Set.range ((↑) : ℝ → ℂ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  smul_mem' := by
    rintro c - ⟨a, rfl⟩
    use c*a
    simp

Submodule 中证明字段末尾的撇号与 LinearMap 中的类似。这些字段以 carrier 字段为基础定义，因为它们在 Membership 实例之前被定义。随后，它们被我们之前看到的 Submodule.add_mem、Submodule.zero_mem 和 Submodule.smul_mem 所取代。

作为操作子空间和线性映射的练习，你将定义线性映射下子空间的原像（pre-image）（当然，后面会看到 Mathlib 已经包含了相关定义）。记住，可以使用 Set.mem_preimage 来对涉及成员资格和原像的陈述进行重写。除了上述关于 LinearMap 和 Submodule 的引理外，这是你唯一需要用到的引理。

def preimage {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) :
    Submodule K V where
  carrier := φ ⁻¹' H
  zero_mem' := by
    dsimp
    sorry
  add_mem' := by
    sorry
  smul_mem' := by
    dsimp
    sorry

使用类型类，Mathlib 知道向量空间的子空间继承了向量空间结构。

example (U : Submodule K V) : Module K U := inferInstance

这个例子很微妙。对象 U 不是一个类型，但 Lean 会通过将其解释为 V 的一个子类型来自动将其强制转换为一个类型。因此，上面的例子可以更明确地重述为：

example (U : Submodule K V) : Module K {x : V // x ∈ U} := inferInstance

9.2.2. 完全格结构和内直和

拥有类型 Submodule K V 而非谓词 IsSubmodule : Set V → Prop 的一个重要好处是，可以方便地赋予 Submodule K V 额外的结构。其中最重要的是它在包含关系下具有完备格结构。例如，不再需要单独的引理来说明两个子空间的交集仍是子空间，我们可以直接使用格的运算符 ⊓ 来构造交集。随后便可对该结构应用任意格论相关的引理。

下面我们验证，两个子空间下确界对应的底层集合，正是它们的（定义上的）交集。

example (H H' : Submodule K V) :
    ((H ⊓ H' : Submodule K V) : Set V) = (H : Set V) ∩ (H' : Set V) := rfl

对底层集合的交集使用不同符号表示可能看起来有些奇怪，但这种对应关系并不适用于上确界运算和集合的并集，因为子空间的并集通常并不是子空间。取而代之的是，需要使用由并集生成的子空间，这通常通过 Submodule.span 来实现。

example (H H' : Submodule K V) :
    ((H ⊔ H' : Submodule K V) : Set V) = Submodule.span K ((H : Set V) ∪ (H' : Set V)) := by
  simp [Submodule.span_union]

另一个细节是，向量空间本身 V 并不属于类型 Submodule K V，因此需要一种方式来表示将 V 视为自身的子空间。这也由格结构提供支持：整个空间作为该格的最大元存在。

example (x : V) : x ∈ (⊤ : Submodule K V) := trivial

同样，这个格的底部元素是唯一元素为零元素的子空间。

example (x : V) : x ∈ (⊥ : Submodule K V) ↔ x = 0 := Submodule.mem_bot K

特别地，我们可以讨论处于（内部）直和的子空间的情况。在两个子空间的情况下，我们使用通用谓词 IsCompl，它适用于任何有界偏序类型。在一般子空间族的情况下，我们使用 DirectSum.IsInternal。

-- 如果两个子空间是直和，则它们生成整个空间。
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊔ V = ⊤ := h.sup_eq_top

-- 如果两个子空间是直和，则它们的交集仅为零。
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊓ V = ⊥ := h.inf_eq_bot

section
open DirectSum
variable {ι : Type*} [DecidableEq ι]

-- 如果子空间是直和，则它们生成整个空间。
example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
  ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top

-- 如果子空间是直和，则它们的交集仅为零。
example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
  (h.submodule_independent.pairwiseDisjoint hij).eq_bot

-- 这些条件表征了直和。
#check DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top

-- 与外直和的关系：如果一族子空间是内直和，则它们的外直和映射到 `V` 的映射是线性同构。
noncomputable example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V)
    (h : DirectSum.IsInternal U) : (⨁ i, U i) ≃ₗ[K] V :=
  LinearEquiv.ofBijective (coeLinearMap U) h
end

9.2.3. 由集合生成的子空间

除了从现有子空间构建子空间，我们还可以使用 Submodule.span K s 从任何集合 s 构建子空间，该函数构建包含 s 的最小子空间。在纸面上，通常使用该空间由 s 的所有线性组合构成的事实。但通常更有效的方法是使用其万有性质，即 Submodule.span_le，以及整个 Galois 连接理论。

example {s : Set V} (E : Submodule K V) : Submodule.span K s ≤ E ↔ s ⊆ E :=
  Submodule.span_le

example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :=
  Submodule.gi K V

当上述方法不够时，可以使用相关的归纳原理 Submodule.span_induction，它保证只要某性质对零元和集合 s 中的元素成立，且在加法和标量乘法下封闭，那么该性质对 s 的张成子空间中的每个元素都成立。

作为练习，我们重新证明 Submodule.mem_sup 的一个推论。记住你可以使用 module 策略，来解决基于 V 上各种代数运算公理的证明目标。

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  induction h using Submodule.span_induction with
  | mem y h =>
      sorry
  | zero =>
      sorry
  | add x y hx hy hx' hy' =>
      sorry
  | smul a x hx hx' =>
      sorry

9.2.4. 拉回和推出子空间

如前所述，我们现在描述如何通过线性映射来拉回和推出子空间。在 Mathlib 中，第一个操作称为 map，第二个操作称为 comap。

section

variable {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W)

variable (E : Submodule K V) in
#check (Submodule.map φ E : Submodule K W)

variable (F : Submodule K W) in
#check (Submodule.comap φ F : Submodule K V)

这些函数定义在 Submodule 命名空间内，因此可以使用点记法写作 E.map φ 而不是``Submodule.map φ E``。不过这种写法阅读起来相当别扭（虽然有些 Mathlib 贡献者会这样写）。特别地，线性映射的像集和核都是子空间，这些特殊情况重要到有专门的声明支持。

example : LinearMap.range φ = .map φ ⊤ := LinearMap.range_eq_map φ

example : LinearMap.ker φ = .comap φ ⊥ := Submodule.comap_bot φ -- or `rfl`

请注意，我们不能写成 φ.ker 来替代 LinearMap.ker φ，因为 LinearMap.ker 不仅适用于线性映射，还适用于保持更多结构的映射类，因此它不期望接收类型以 LinearMap 开头的参数，所以点记法在这里无法使用。然而，在右侧我们能够使用另一种点记法。因为 Lean 在展开左侧后，期望得到类型为 Submodule K V 的项，因此它会将 .comap 解析为 Submodule.comap。

以下引理描述了这些子模与线性映射 φ 的关键关系。

open Function LinearMap

example : Injective φ ↔ ker φ = ⊥ := ker_eq_bot.symm

example : Surjective φ ↔ range φ = ⊤ := range_eq_top.symm

作为练习，我们来证明 map 和 comap 的 Galois 连接性质。可以使用以下引理，但这不是必需的，因为它们是根据定义成立的。

#check Submodule.mem_map_of_mem
#check Submodule.mem_map
#check Submodule.mem_comap

example (E : Submodule K V) (F : Submodule K W) :
    Submodule.map φ E ≤ F ↔ E ≤ Submodule.comap φ F := by
  sorry

9.2.5. 商空间

商向量空间使用通用的商记号（输入为 quot，而非普通的 /）。投影到商空间的映射是 Submodule.mkQ，其万有性质由 Submodule.liftQ 给出。

variable (E : Submodule K V)

example : Module K (V ⧸ E) := inferInstance

example : V →ₗ[K] V ⧸ E := E.mkQ

example : ker E.mkQ = E := E.ker_mkQ

example : range E.mkQ = ⊤ := E.range_mkQ

example (hφ : E ≤ ker φ) : V ⧸ E →ₗ[K] W := E.liftQ φ hφ

example (F : Submodule K W) (hφ : E ≤ .comap φ F) : V ⧸ E →ₗ[K] W ⧸ F := E.mapQ F φ hφ

noncomputable example : (V ⧸ LinearMap.ker φ) ≃ₗ[K] range φ := φ.quotKerEquivRange

作为练习，我们来证明商空间子空间的对应定理。Mathlib 中有一个稍微更精确的版本，称为 Submodule.comapMkQRelIso。

open Submodule

#check Submodule.map_comap_eq
#check Submodule.comap_map_eq

example : Submodule K (V ⧸ E) ≃ { F : Submodule K V // E ≤ F } where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

9.3. 自同态

线性映射中的一个重要特例是自同态（endomorphisms）：即从向量空间自身映射到自身的线性映射。自同态特别有趣，因为它们构成了一个 K-代数。具体来说，我们可以在其上对系数属于 K 的多项式进行求值，它们也可能具有特征值和特征向量。

Mathlib 使用简称 Module.End K V := V →ₗ[K] V，这在大量使用此类映射时非常方便，尤其是在打开了 Module 命名空间后。

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

variable {W : Type*} [AddCommGroup W] [Module K W]


open Polynomial Module LinearMap

example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ :=
  LinearMap.mul_eq_comp φ ψ -- `rfl` 也可以

-- evaluating `P` on `φ`
example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
  aeval φ P

-- evaluating `X` on `φ` gives back `φ`
example (φ : End K V) : aeval φ (X : K[X]) = φ :=
  aeval_X φ

作为练习，结合自同态、子空间和多项式的操作，让我们证明二元核引理：对于任意自同态 \(φ\) 及互素多项式 \(P\) 和 \(Q\)，有 \(\ker P(φ) ⊕ \ker Q(φ) = \ker \big(PQ(φ)\big)\)。

注意，IsCoprime x y 的定义为 ∃ a b, a * x + b * y = 1 。

#check Submodule.eq_bot_iff
#check Submodule.mem_inf
#check LinearMap.mem_ker

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) : ker (aeval φ P) ⊓ ker (aeval φ Q) = ⊥ := by
  sorry

#check Submodule.add_mem_sup
#check map_mul
#check LinearMap.mul_apply
#check LinearMap.ker_le_ker_comp

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P*Q)) := by
  sorry

我们现在转向本征空间和特征值的讨论。对于自同态 \(φ\) 和标量 \(a\) ，与之对应的本征空间是 \(φ - aId\) 的核空间。本征空间对所有 a 都有定义，但只有在本征空间非零时才有意义。然而，本征向量定义为本征空间中的非零元素。对应的谓词是 End.HasEigenvector。

example (φ : End K V) (a : K) : φ.eigenspace a = LinearMap.ker (φ - a • 1) :=
  End.eigenspace_def

然后有一个谓词 End.HasEigenvalue 和对应的子类型 End.Eigenvalues。

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ φ.eigenspace a ≠ ⊥ :=
  Iff.rfl

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ ∃ v, φ.HasEigenvector a v  :=
  ⟨End.HasEigenvalue.exists_hasEigenvector, fun ⟨_, hv⟩ ↦ φ.hasEigenvalue_of_hasEigenvector hv⟩

example (φ : End K V) : φ.Eigenvalues = {a // φ.HasEigenvalue a} :=
  rfl

-- 特征值是最小多项式的根
example (φ : End K V) (a : K) : φ.HasEigenvalue a → (minpoly K φ).IsRoot a :=
  φ.isRoot_of_hasEigenvalue

-- 有限维情况下，反之亦然（我们将在下面讨论维度）
example [FiniteDimensional K V] (φ : End K V) (a : K) :
    φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
  φ.hasEigenvalue_iff_isRoot

-- Cayley-Hamilton
example [FiniteDimensional K V] (φ : End K V) : aeval φ φ.charpoly = 0 :=
  φ.aeval_self_charpoly

9.4. 矩阵、基和维度

9.4.1. 矩阵

在介绍抽象向量空间的基之前，我们先回到更基础的线性代数设置——定义在某域 \(K\) 上的 \(K^n\) 。这里的主要对象是向量和矩阵。对于具体向量，可以使用 ![…] 记法，分量之间用逗号分隔。对于具体矩阵，可以使用 !![…] 记法，行之间用分号分隔，行内分量用冒号分隔。当矩阵元素类型是可计算类型（例如 ℕ 或 ℚ）时，可以使用 eval 命令来进行基本运算操作的试验。

section matrices

-- Adding vectors
#eval !![1, 2] + !![3, 4]  -- !![4, 6]

-- Adding matrices
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

-- Multiplying matrices
#eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

需要理解的是，#eval 的使用主要用于探索和试验，并不旨在替代如 Sage 这类计算机代数系统。这里矩阵的数据表示方式并不在计算上高效，它采用函数而非数组，优化目标是证明而非计算。而且，#eval 所用的虚拟机也未针对这种用途进行优化。

请注意，矩阵表示中列出了多行，而向量表示既不是行向量也不是列向量。矩阵与向量的乘法，若从左乘，则将向量视为行向量；若从右乘，则将向量视为列向量。

对应的操作为：

Matrix.vecMul，符号为 ᵥ*
Matrix.mulVec，符号为 *ᵥ

这些符号限定在 Matrix 命名空间，因此我们需要打开该命名空间才能使用。

open Matrix

-- 矩阵左作用于向量
#eval !![1, 2; 3, 4] *ᵥ ![1, 1] -- ![3, 7]

-- 矩阵左作用于向量，结果为一维矩阵
#eval !![1, 2] *ᵥ ![1, 1]  -- ![3]

-- 矩阵右作用于向量
#eval  ![1, 1, 1] ᵥ* !![1, 2; 3, 4; 5, 6] -- ![9, 12]

为了生成由某向量指定的相同行或列的矩阵，我们使用 Matrix.row 和 Matrix.column，它们的参数分别是用于索引行或列的类型以及该向量。例如，可以得到单行矩阵或单列矩阵（更准确地说，是行或列由 Fin 1 索引的矩阵）。

#eval row (Fin 1) ![1, 2] -- !![1, 2]

#eval col (Fin 1) ![1, 2] -- !![1; 2]

其它熟悉的操作包括向量点积、矩阵转置，以及对于方阵的行列式和迹。

-- 向量点积
#eval ![1, 2] ⬝ᵥ ![3, 4] -- `11`

-- 矩阵转置
#eval !![1, 2; 3, 4]ᵀ -- `!![1, 3; 2, 4]`

-- 行列式
#eval !![(1 : ℤ), 2; 3, 4].det -- `-2`

-- 迹
#eval !![(1 : ℤ), 2; 3, 4].trace -- `5`

当矩阵元素类型不可计算时，比如实数，#eval 就无能为力了。而且，这类计算也不能直接用于证明中，否则需要大幅扩展受信任代码库（即在检验证明时必须信任的 Lean 核心部分）。

因此，在证明中推荐使用 simp 和 norm_num 策略，或者它们对应的命令形式来进行快速探索和简化。

#simp !![(1 : ℝ), 2; 3, 4].det -- `4 - 2*3`

#norm_num !![(1 : ℝ), 2; 3, 4].det -- `-2`

#norm_num !![(1 : ℝ), 2; 3, 4].trace -- `5`

variable (a b c d : ℝ) in
#simp !![a, b; c, d].det -- `a * d – b * c`

下一个关于方阵的重要操作是求逆。类似于数的除法总是定义的，且对除以零的情况返回人为设定的零值，矩阵求逆操作也定义在所有矩阵上，对于不可逆矩阵返回零矩阵。

更具体地，存在一个通用函数 Ring.inverse，它在任意环中实现此功能；对于任意矩阵 A，其逆矩阵定义为 Ring.inverse A.det • A.adjugate 根据Cramer’s rule，当矩阵行列式不为零时，上述定义确实是矩阵 A 的逆矩阵。

#norm_num [Matrix.inv_def] !![(1 : ℝ), 2; 3, 4]⁻¹ -- !![-2, 1; 3 / 2, -(1 / 2)]

当然这种定义确实只对可逆矩阵有用。存在一个通用类型类 Invertible 来帮助记录这一点。例如，下面例子中的 simp 调用将使用 inv_mul_of_invertible 引理，该引理具有 Invertible 类型类假设，因此只有在类型类合成系统能够找到它时才会触发。在这里，我们使用 have 语句使这一事实可用。

example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  have : Invertible !![(1 : ℝ), 2; 3, 4] := by
    apply Matrix.invertibleOfIsUnitDet
    norm_num
  simp

在这个完全具体的例子中，我们也可以使用 norm_num 工具，和 apply? 来找到最后一行：

example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  norm_num [Matrix.inv_def]
  exact one_fin_two.symm

之前所有具体矩阵的行和列均由某个 Fin n 索引（行列的 n 不一定相同）。但有时使用任意有限类型作为矩阵的行列索引更为方便。例如，有限图的邻接矩阵，其行和列自然由图的顶点索引。

实际上，如果仅定义矩阵而不涉及运算，索引类型的有限性甚至不是必须的，矩阵元素的类型也无需具备任何代数结构。因此，Mathlib 直接将 Matrix m n α 定义为 m → n → α，其中 m、n、α 是任意类型。我们之前使用的矩阵类型多如 Matrix (Fin 2) (Fin 2) ℝ。当然，代数运算对 m、n 和 α 有更严格的假设。

我们不直接使用 m → n → α 的主要原因，是让类型类系统能正确理解我们的意图。举例来说，对于环 R，类型 n → R 自带逐点乘法（point-wise multiplication），而 m → n → R 也有类似操作，但这并不是我们想在矩阵上使用的乘法。

下面第一个示例中，我们强制 Lean 展开 Matrix 定义，接受陈述的意义，并通过逐个元素检查完成证明。

而后面两个示例展示了 Lean 对 Fin 2 → Fin 2 → ℤ 使用逐点乘法，而对 Matrix (Fin 2) (Fin 2) ℤ 使用矩阵乘法。

section

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) * (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : !![1, 1; 1, 1] * !![1, 1; 1, 1] = !![2, 2; 2, 2] := by
  norm_num

为了定义矩阵作为函数而不失去 Matrix 在类型类合成中的好处，我们可以使用函数和矩阵之间的等价关系 Matrix.of。这个等价关系是通过 Equiv.refl 隐式定义的。

例如，我们可以定义与向量 v 对应的范德蒙德矩阵。

example {n : ℕ} (v : Fin n → ℝ) :
    Matrix.vandermonde v = Matrix.of (fun i j : Fin n ↦ v i ^ (j : ℕ)) :=
  rfl
end
end matrices

9.4.2. 基

我们现在讨论向量空间的基。非正式地说，这一概念有多种定义方式：

可以通过万有性质来定义；
可以说基是一族线性无关且张成全空间的向量；
或结合这两个性质，直接说基是一族向量，使得每个向量都能唯一地表示为基向量的线性组合；
另一种说法是，基提供了与基域 K 的某个幂（作为 K 上的向量空间）的线性同构。

实际上，Mathlib 在底层采用的是最后一种同构的定义，并从中推导出其他性质。对于无限基的情况，需稍加注意“基域的幂”这一说法。因为在代数环境中，只考虑有限线性组合有意义，所以我们参考的向量空间不是基域的直积，而是直和。我们可以用 ⨁ i : ι, K 表示某个类型 ι 索引的基向量集合对应的直和，但更常用的是更专门的表示法 ι →₀ K，表示“具有有限支集的函数”，即在 ι 上除有限点外值为零的函数（这个有限集合不是固定的，依赖于函数本身）。

对于基 B 中的函数，给定向量 v 和索引 i : ι，函数的值即为 v 在第 i 个基向量上的坐标分量。

以类型 ι 索引的向量空间 V 的基类型为 Basis ι K V，对应的同构称为 Basis.repr。

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

section

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)

-- 索引为 ``i`` 的基向量
#check (B i : V)

-- 与模空间 ``B`` 给出的线性同构
#check (B.repr : V ≃ₗ[K] ι →₀ K)

-- ``v`` 的分量函数
#check (B.repr v : ι →₀ K)

-- ``v`` 在索引为 ``i`` 的基向量上的分量
#check (B.repr v i : K)

与其从同构出发，也可以从一族线性无关且张成的向量族 b 开始构造基，这就是 Basis.mk。“张成”的假设表达为 ⊤ ≤ Submodule.span K (Set.range b)，这里的 ⊤ 是 V 的最大子模，即 V 自身作为自身的子模。这个表达看起来有些拗口，但下面我们将看到它与更易理解的表达式 ∀ v, v ∈ Submodule.span K (Set.range b) 几乎是定义等价的（下面代码中的下划线表示无用信息 v ∈ ⊤）。

noncomputable example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) : Basis ι K V :=
  Basis.mk b_indep (fun v _ ↦ b_spans v)

-- 该基的底层向量族确实是 ``b``。
example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) (i : ι) :
    Basis.mk b_indep (fun v _ ↦ b_spans v) i = b i :=
  Basis.mk_apply b_indep (fun v _ ↦ b_spans v) i

特别地，模型向量空间 ι →₀ K 具有所谓的标准基（canonical basis），其 repr 函数在任意向量上的值即为恒等同构。该基称为 Finsupp.basisSingleOne，其中 Finsupp 表示有限支集函数，basisSingleOne 指的是基向量是除单个输入点外，其余点值皆为零的函数。更具体地，索引为 i : ι 的基向量是 Finsupp.single i 1，这是一个有限支集函数，在点 i 取值为 1，其余点取值为 0。

variable [DecidableEq ι]

example : Finsupp.basisSingleOne.repr = LinearEquiv.refl K (ι →₀ K) :=
  rfl

example (i : ι) : Finsupp.basisSingleOne i = Finsupp.single i 1 :=
  rfl

当索引类型是有限集合时，有限支集函数的概念就不再需要。这时，我们可以使用更简单的 Pi.basisFun，它直接构造了整个 ι → K 的一组基。

example [Finite ι] (x : ι → K) (i : ι) : (Pi.basisFun K ι).repr x i = x i := by
  simp

回到抽象向量空间基的通用情况，我们可以将任何向量表示为基向量的线性组合。让我们首先看看有限基的简单情况。

example [Fintype ι] : ∑ i : ι, B.repr v i • (B i) = v :=
  B.sum_repr v

当索引类型 ι 不是有限集时，上述直接对 ι 求和的说法在理论上没有意义，因为无法对无限集合进行直接求和。不过，被求和的函数的支集是有限的（即 B.repr v 的支集），这就允许对有限支集进行求和。为了处理这种情况，Mathlib 使用了一个特殊的函数，虽然需要一些时间适应，它是 Finsupp.linearCombination`（建立在更通用的 `Finsupp.sum 之上）。

给定一个从类型 ι 到基域 K 的有限支集函数 c，以及任意从 ι 到向量空间 V 的函数 f，Finsupp.linearCombination K f c 定义为对 c 的支集上所有元素的 c • f 进行标量乘法后求和。特别地，我们也可以将求和范围替换为任何包含 c 支集的有限集合。

When ι is not finite, the above statement makes no sense a priori: we cannot take a sum over ι. However the support of the function being summed is finite (it is the support of B.repr v). But we need to apply a construction that takes this into account. Here Mathlib uses a special purpose function that requires some time to get used to: Finsupp.linearCombination (which is built on top of the more general Finsupp.sum). Given a finitely supported function c from a type ι to the base field K and any function f from ι to V, Finsupp.linearCombination K f c is the sum over the support of c of the scalar multiplication c • f. In particular, we can replace it by a sum over any finite set containing the support of c.

example (c : ι →₀ K) (f : ι → V) (s : Finset ι) (h : c.support ⊆ s) :
    Finsupp.linearCombination K f c = ∑ i ∈ s, c i • f i :=
  Finsupp.linearCombination_apply_of_mem_supported K h

也可以假设 f 是有限支集函数，这样依然能得到良定义的求和结果。但 Finsupp.linearCombination 所作的选择更贴合我们关于基的讨论，因为它支持陈述 Basis.sum_repr 的推广版本。

example : Finsupp.linearCombination K B (B.repr v) = v :=
  B.linearCombination_repr v

你可能会好奇，为什么这里的 K 是显式参数，尽管它可以从 c 的类型中推断出来。关键在于，部分应用的 Finsupp.linearCombination K f 本身就是一个有趣的对象。它不仅仅是一个从 ι →₀ K 到 V 的普通函数，更是一个 K-线性映射。

variable (f : ι → V) in
#check (Finsupp.linearCombination K f : (ι →₀ K) →ₗ[K] V)

上述细节也解释了为什么不能用点记法写成 c.linearCombination K f 来代替 Finsupp.linearCombination K f c。事实上，Finsupp.linearCombination 本身并不直接接收 c 作为参数，而是先部分应用 K 和 f，得到一个被强制转换为函数类型的对象，随后该函数才接收 c 作为参数。

回到数学讨论，理解基下向量的具体表示在形式化数学中往往没有你想象的那么有用非常重要。实际上，直接利用基的更抽象性质通常更加高效。特别是，基的通用性质将其与代数中的其他自由对象连接起来，使得我们可以通过指定基向量的像来构造线性映射。这就是 Basis.constr。对于任意 K-向量空间 W，我们的基 B 提供了一个线性同构 Basis.constr B K : (ι → W) ≃ₗ[K] (V →ₗ[K] W)。该同构的特点是，对于任意函数 u : ι → W，它对应的线性映射将基向量 B i 映射为 u i，其中 i : ι。

section

variable {W : Type*} [AddCommGroup W] [Module K W]
         (φ : V →ₗ[K] W) (u : ι → W)

#check (B.constr K : (ι → W) ≃ₗ[K] (V →ₗ[K] W))

#check (B.constr K u : V →ₗ[K] W)

example (i : ι) : B.constr K u (B i) = u i :=
  B.constr_basis K u i

这个性质实际上是特征性的，因为线性映射是由它们在基上的值决定的：

example (φ ψ : V →ₗ[K] W) (h : ∀ i, φ (B i) = ψ (B i)) : φ = ψ :=
  B.ext h

如果我们在目标空间上也有一个基 B'，那么我们可以将线性映射与矩阵进行识别。这种识别是一个 K-线性同构。

variable {ι' : Type*} (B' : Basis ι' K W) [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι']

open LinearMap

#check (toMatrix B B' : (V →ₗ[K] W) ≃ₗ[K] Matrix ι' ι K)

open Matrix -- 获取对矩阵和向量之间乘法的 ``*ᵥ`` 记法的访问。

example (φ : V →ₗ[K] W) (v : V) : (toMatrix B B' φ) *ᵥ (B.repr v) = B'.repr (φ v) :=
  toMatrix_mulVec_repr B B' φ v

variable {ι'' : Type*} (B'' : Basis ι'' K W) [Fintype ι''] [DecidableEq ι'']

example (φ : V →ₗ[K] W) : (toMatrix B B'' φ) = (toMatrix B' B'' .id) * (toMatrix B B' φ) := by
  simp

end

作为本主题的练习，我们将证明一部分定理，保证自同态的行列式是良定义的。具体来说，我们要证明：当两个基由相同类型索引时，它们对应任意自同态的矩阵具有相同的行列式。然后，结合所有基的索引类型彼此线性同构，便可得到完整结论。

当然，Mathlib 已经包含了这一结论，且 simp 策略可以立即解决此目标，因此你不应过早使用它，而应先尝试使用相关引理进行证明。

open Module LinearMap Matrix

-- 一些来自于 `LinearMap.toMatrix` 是一个代数同态的事实的引理。
#check toMatrix_comp
#check id_comp
#check comp_id
#check toMatrix_id

-- 一些来自于 ``Matrix.det`` 是一个乘法单元环同态的事实的引理。
#check Matrix.det_mul
#check Matrix.det_one

example [Fintype ι] (B' : Basis ι K V) (φ : End K V) :
    (toMatrix B B φ).det = (toMatrix B' B' φ).det := by
  set M := toMatrix B B φ
  set M' := toMatrix B' B' φ
  set P := (toMatrix B B') LinearMap.id
  set P' := (toMatrix B' B) LinearMap.id
  sorry
end

9.4.3. 维度

回到单个向量空间的情况，基也用于定义维度的概念。在这里，我们再次遇到有限维向量空间的基本情况。对于这样的空间，我们期望维度是一个自然数。这就是 Module.finrank。它将基域作为显式参数，因为给定的阿贝尔群可以是不同域上的向量空间。

section
#check (Module.finrank K V : ℕ)

-- `Fin n → K` 是维度为 `n` 的典型空间。
example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
  Module.finrank_fin_fun K

-- 作为自身的向量空间，`ℂ` 的维度为1。
example : Module.finrank ℂ ℂ = 1 :=
  Module.finrank_self ℂ

-- 但作为实向量空间，它的维度为2。
example : Module.finrank ℝ ℂ = 2 :=
  Complex.finrank_real_complex

注意到 Module.finrank 是为任何向量空间定义的。它对于无限维向量空间返回零，就像除以零返回零一样。

当然，许多引理都需要有限维度的假设。这就是 FiniteDimensional 类型类的作用。例如，考虑下一个例子在没有这个假设的情况下是如何失败的。

example [FiniteDimensional K V] : 0 < Module.finrank K V ↔ Nontrivial V  :=
  Module.finrank_pos_iff

在上述陈述中，Nontrivial V 表示 V 至少包含两个不同元素。注意，Module.finrank_pos_iff 没有显式参数。从左向右使用时没问题，但从右向左使用时会遇到困难，因为 Lean 无法从 Nontrivial V 这一命题中推断出域 K。此时，使用命名参数语法会很有帮助，前提是确认该引理是在一个名为 R 的环上陈述的。因此我们可以写成：

example [FiniteDimensional K V] (h : 0 < Module.finrank K V) : Nontrivial V := by
  apply (Module.finrank_pos_iff (R := K)).1
  exact h

上述写法看起来有些奇怪，因为我们已经有了假设 h，因此完全可以直接写成 Module.finrank_pos_iff.1 h 来使用该引理。不过，了解命名参数的用法对于更复杂的情况仍然很有帮助。

根据定义，FiniteDimensional K V 可以通过任意一组基来判定。

variable {ι : Type*} (B : Basis ι K V)

example [Finite ι] : FiniteDimensional K V := FiniteDimensional.of_fintype_basis B

example [FiniteDimensional K V] : Finite ι :=
  (FiniteDimensional.fintypeBasisIndex B).finite
end

使用与线性子空间对应的子类型具有向量空间结构，我们可以讨论子空间的维度。

section
variable (E F : Submodule K V) [FiniteDimensional K V]

open Module

example : finrank K (E ⊔ F : Submodule K V) + finrank K (E ⊓ F : Submodule K V) =
    finrank K E + finrank K F :=
  Submodule.finrank_sup_add_finrank_inf_eq E F

example : finrank K E ≤ finrank K V := Submodule.finrank_le E

在第一条语句中，类型注释的目的是确保对 Type* 的强制转换不会过早触发。

我们现在准备进行一个关于 finrank 和子空间的练习。

example (h : finrank K V < finrank K E + finrank K F) :
    Nontrivial (E ⊓ F : Submodule K V) := by
  sorry
end

我们现在转向一般的维数理论情形。此时，finrank 就不再适用，但我们依然知道，对于同一向量空间的任意两组基，其索引类型之间存在一个双射。因此，我们仍然可以期望将秩定义为基数（cardinal），即“类型集合在存在双射的等价关系下的商集”中的元素。

在讨论基数时，难以像本书其他部分那样忽略类似罗素悖论的基础性问题。因为不存在“所有类型的类型”，否则会导致逻辑矛盾。这一问题通过宇宙层级（universe hierarchy）来解决，而我们通常会尝试忽略这些细节。

每个类型都有一个宇宙层级，该层级行为类似自然数。特别地，有一个零层级，对应的宇宙 Type 0 简写为 Type，这个宇宙足以容纳几乎所有经典数学对象，比如 ℕ 和 ℝ 都属于类型 Type。每个层级 u 有一个后继层级 u + 1，且 Type u 的类型是 Type (u + 1)。

但宇宙层级不是自然数，它们本质不同且没有对应的类型。例如，无法在 Lean 中声明 u ≠ u + 1，因为不存在一个类型可以表达这个命题。即使声明 Type u ≠ Type (u+1) 也没有意义，因为两者属于不同的类型。

当我们写 Type* 时，Lean 会自动插入一个名为 u_n 的宇宙变量，其中 n 是一个数字，允许定义和陈述在所有宇宙层级中成立。

给定宇宙层级 u，我们可以在 Type u 上定义等价关系：当且仅当两个类型 α 和 β 存在双射时它们等价。商类型 Cardinal.{u} 属于 Type (u + 1)，花括号表示这是一个宇宙变量。类型 α : Type u 在商中的像为 Cardinal.mk α : Cardinal.{u}。

但我们不能直接比较不同宇宙层级中的基数。因此技术上讲，不能将向量空间 V 的秩定义为索引 V 基的所有类型的基数。相反，秩定义为 Module.rank K V，即 V 中所有线性无关集基数的上确界。如果 V 属于宇宙层级 u，则其秩属于 Cardinal.{u} 类型。

#check V -- Type u_2
#check Module.rank K V -- Cardinal.{u_2}

这个定义仍然可以与基联系起来。实际上，宇宙层级上存在一个交换的 max 运算，对于任意两个宇宙层级 u 和 v，存在一个操作 Cardinal.lift.{u, v} : Cardinal.{v} → Cardinal.{max v u}，该操作允许将基数提升到共同的宇宙层级中，从而陈述维数定理。

universe u v -- `u` 和 `v` 将表示宇宙层级

variable {ι : Type u} (B : Basis ι K V)
         {ι' : Type v} (B' : Basis ι' K V)

example : Cardinal.lift.{v, u} (.mk ι) = Cardinal.lift.{u, v} (.mk ι') :=
  mk_eq_mk_of_basis B B'

我们可以将有限维情况与此讨论联系起来，使用从自然数到有限基数的强制转换（更准确地说，是生活在 Cardinal.{v} 中的有限基数，其中 v 是 V 的宇宙层级）。

example [FiniteDimensional K V] :
    (Module.finrank K V : Cardinal) = Module.rank K V :=
  Module.finrank_eq_rank K V