第10章线性代数 - 深度伴读

本章定位

本章是 Mathlib 线性代数库的入门，核心内容：

向量空间与线性映射：Module K V、V →ₗ[K] W

直和与直积：二元积、任意族直和/积的泛性质

子空间与商空间：Submodule 完备格、V ⧸ E

自同态：多项式求值、特征值/特征空间、Cayley-Hamilton

矩阵：!![...] 语法、运算、逆矩阵

基与维数：Basis ι K V、finrank、无限维的 rank

本章概念密集，建议分块学习。

10.1 向量空间与线性映射

核心洞见

Lean 中向量空间 = AddCommGroup V + Module K V。必须分开写两个类型类，不能写 extends，否则 Lean 会尝试搜索未指定的域 K。

10.1.1 向量空间

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
 
-- 标量乘法记为 •
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

module tactic

module tactic 自动证明由向量空间公理推出的目标，类似 ring/group。引理命名中标量乘法常缩写为 smul。

Mathlib 的线性代数实际上覆盖半环上的模，这比向量空间更一般：

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

10.1.2 线性映射

线性映射是 bundled 的：V →ₗ[K] W 包含函数 + 线性性证明。

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-向量空间
#check (2 • φ + ψ : V →ₗ[K] W)

线性映射复合用 ∘ₗ，不是 ∘

variable (θ : W →ₗ[K] V)
#check (φ.comp θ : W →ₗ[K] W)
#check (φ ∘ₗ θ : W →ₗ[K] W)   -- 推荐

构造线性映射（结构骨架生成器）：

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

map_add' vs map_add

map_add' 用 toFun 表述，map_add 用 coercion 到函数表述。根命名空间里的 map_add 适用于所有保持加法的 bundled 映射（加群同态、线性映射、连续线性映射等）。

组合子构造：

-- 标量乘法映射：K →ₗ[K] V →ₗ[K] V
#check (LinearMap.lsmul K V 3 : V →ₗ[K] V)
#check (LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V)

线性同构 V ≃ₗ[K] W：

example (f : V ≃ₗ[K] W) : f ≪≫ₗ f.symm = LinearEquiv.refl K V :=
  f.self_trans_symm
 
-- 从双射构造同构（noncomputable）
noncomputable example (f : V →ₗ[K] W) (h : Function.Bijective f) : V ≃ₗ[K] W :=
  .ofBijective f h

10.1.3 直和与直积

二元直和/直积：对两个空间，直和 = 直积 = V × W。

-- 投影
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 : 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 ψ

任意族的直和与直积：

open DirectSum
 
variable {ι : Type*} [DecidableEq ι]
         (V : ι → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
 
-- 从直和到 W 的映射
example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
  DirectSum.toModule K ι W φ
 
-- 从 W 到直积的映射
example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
  LinearMap.pi φ
 
-- 有限型时，直和与直积同构
example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
  linearEquivFunOnFintype K ι V

DirectSum 记号需要 open DirectSum

⨁ 在 DirectSum 命名空间中。DecidableEq ι 是技术性的实现要求。

10.2 子空间与商空间

核心洞见

Submodule K V 是类型，不是谓词。它自动 coercion 到 Set V，成员用 ∈。

10.2.1 子空间

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

构造子空间：ℝ 作为 ℂ 的 ℝ-子空间

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

rintro + use + simp 模式

与第9章子群构造完全一致。先 rintro 拆解，再 use 提供见证，最后 simp 化简。

子空间继承向量空间结构：

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

10.2.2 完备格结构

-- ⊓ = 交集（子空间的交仍是子空间）
example (H H' : Submodule K V) :
    ((H ⊓ H' : Submodule K V) : Set V) = (H : Set V) ∩ (H' : Set V) := rfl
 
-- ⊔ = 生成子空间（不是并集！）
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]
 
-- ⊤ = 整个空间
example (x : V) : x ∈ (⊤ : Submodule K V) := trivial
 
-- ⊥ = 零子空间 {0}
example (x : V) : x ∈ (⊥ : Submodule K V) ↔ x = 0 := Submodule.mem_bot K

内部直和：

-- 两个子空间的直和
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
 
-- 一族子空间的内部直和
example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
    ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top

10.2.3 由集合生成的子空间

-- span s = 包含 s 的最小子空间
example {s : Set V} (E : Submodule K V) : Submodule.span K s ≤ E ↔ s ⊆ E :=
  Submodule.span_le
 
-- Galois insertion：span 与 coercion 形成 Galois 连接
example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :=
  Submodule.gi K V
 
-- 归纳原理
example {s : Set V} {p : V → Prop} (h0 : p 0)
    (hs : ∀ x ∈ s, p x)
    (hadd : ∀ x y, p x → p y → p (x + y))
    (hsmul : ∀ a x, p x → p (a • x)) :
    ∀ x ∈ Submodule.span K s, p x :=
  Submodule.span_induction h0 hs hadd hsmul

10.2.4 推前与拉回

variable (φ : V →ₗ[K] W)
 
-- map = 推前（像）
#check (Submodule.map φ E : Submodule K W)
 
-- comap = 拉回（原像）
#check (Submodule.comap φ F : Submodule K V)
 
-- 核与像
example : LinearMap.range φ = .map φ ⊤ := LinearMap.range_eq_map φ
example : LinearMap.ker φ = .comap φ ⊥ := Submodule.comap_bot φ
 
-- 单射/满射的刻画
example : Injective φ ↔ ker φ = ⊥ := ker_eq_bot.symm
example : Surjective φ ↔ range φ = ⊤ := range_eq_top.symm
 
-- Galois 连接
example (E : Submodule K V) (F : Submodule K W) :
    Submodule.map φ E ≤ F ↔ E ≤ Submodule.comap φ F := by
  sorry  -- 练习

不能用 φ.ker

LinearMap.ker 也适用于更一般的映射类，不期望参数类型以 LinearMap 开头，所以点记法 φ.ker 不行。但 φ.range 可以。

10.2.5 商空间

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
 
-- 万有性质：核包含 E 的映射可下降到商
example (hφ : E ≤ ker φ) : V ⧸ E →ₗ[K] W := E.liftQ φ hφ
 
-- 第一同构定理
noncomputable example : (V ⧸ LinearMap.ker φ) ≃ₗ[K] range φ := φ.quotKerEquivRange

商空间记号

⧸ 是特殊 unicode（\quot），不是普通斜杠 /。

10.3 自同态

核心洞见

自同态 End K V 构成 K-代数，可以代入多项式，有特征值和特征向量。

10.3.1 基本定义

open Polynomial Module LinearMap End
 
-- End K V = V →ₗ[K] V
example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ := End.mul_eq_comp φ ψ
 
-- 多项式求值
example (P : K[X]) (φ : End K V) : V →ₗ[K] V := aeval φ P
 
-- 代入 X 得到原映射
example (φ : End K V) : aeval φ (X : K[X]) = φ := aeval_X φ

10.3.2 核引理（重要练习）

对互素多项式 P 和 Q，有 ker P(φ) ⊕ ker Q(φ) = ker (PQ)(φ)：

-- 核的交为零
example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊓ ker (aeval φ Q) = ⊥ := by sorry
 
-- 核的直和为积的核
example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P * Q)) := by sorry

IsCoprime

IsCoprime P Q 定义为 ∃ a b, a * P + b * Q = 1。

10.3.3 特征值与特征空间

-- 特征空间 = ker(φ - a·Id)
example (φ : End K V) (a : K) : φ.eigenspace a = LinearMap.ker (φ - a • 1) :=
  End.eigenspace_def
 
-- 特征值 ⇔ 特征空间非零
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

10.3.4 极小多项式与 Cayley-Hamilton

-- 特征值是极小多项式的根
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

10.4 矩阵、基与维数

10.4.1 矩阵

具体矩阵语法：

-- 向量
#eval ![1, 2] + ![3, 4]  -- ![4, 6]
 
-- 矩阵：行之间用分号，列之间用逗号
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]
#eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![13, 16; 29, 36]

矩阵与向量乘法：

open Matrix
 
-- 矩阵在左，向量在右（把向量当作列向量）
#eval !![1, 2; 3, 4] *ᵥ ![1, 1]  -- ![3, 7]
 
-- 向量在左，矩阵在右（把向量当作行向量）
#eval ![1, 1, 1] ᵥ* !![1, 2; 3, 4; 5, 6]  -- ![9, 12]

向量记号的歧义

![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

证明中的矩阵：

#simp !![(1 : ℝ), 2; 3, 4].det  -- `4 - 2*3`
#norm_num !![(1 : ℝ), 2; 3, 4].det  -- `-2`
 
-- 含参数的矩阵
variable (a b c d : ℝ) in
#simp !![a, b; c, d].det  -- `a * d - b * c`

矩阵求逆：

#norm_num [Matrix.inv_def] !![(1 : ℝ), 2; 3, 4]⁻¹
-- !![-2, 1; 3/2, -(1/2)]
 
-- 证明逆矩阵
example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  have : Invertible !![(1 : ℝ), 2; 3, 4] := by
    apply Matrix.invertibleOfIsUnitDet
    norm_num
  simp

非可逆矩阵的逆

Lean 中所有矩阵都有逆，非可逆时返回零矩阵（类似 1/0 = 0 的设计）。 A⁻¹ = Ring.inverse A.det • A.adjugate，由 Cramer 法则定义。

一般索引类型：

-- Matrix m n α = m → n → α（对任意类型 m, n, α）
example {n : ℕ} (v : Fin n → ℝ) :
    Matrix.vandermonde v = Matrix.of (fun i j : Fin n ↦ v i ^ (j : ℕ)) :=
  rfl

为什么不用 m → n → α 直接？

因为 m → n → R 会被赋予逐点乘法，而矩阵乘法是另一种运算。Matrix 类型包装让类型类系统正确选择运算。

10.4.2 基

Basis ι K V：由类型 ι 索引的 V 的 K-基。

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)
 
-- 基向量
#check (B i : V)
 
-- 坐标同构：V ≃ₗ[K] ι →₀ K（有限支撑函数）
#check (B.repr : V ≃ₗ[K] ι →₀ K)
 
-- v 的坐标函数
#check (B.repr v : ι →₀ K)
 
-- v 在基向量 i 上的分量
#check (B.repr v i : K)

ι →₀ K

“有限支撑函数” = 只在有限个点上非零的函数。对无限基，只能做有限线性组合。

从线性无关且张成的族构造基：

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)

⊤ ≤ Submodule.span K (Set.range b) 的含义

⊤ 是 V 作为自身的子空间。⊤ ≤ span 等价于 ∀ v, v ∈ span，即张成整个空间。

典范基：

-- ι →₀ K 的典范基：基向量是 Finsupp.single i 1
example [DecidableEq ι] (i : ι) : Finsupp.basisSingleOne i = Finsupp.single i 1 := rfl
 
-- 有限型时，ι → 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
 
-- 一般情况：用 Finsupp.linearCombination
example : Finsupp.linearCombination K B (B.repr v) = v :=
  B.linearCombination_repr v
 
-- linearCombination 本身是线性映射
#check (Finsupp.linearCombination K B : (ι →₀ K) →ₗ[K] V)

基的泛性质——构造线性映射：

variable {W : Type*} [AddCommGroup W] [Module K W] (u : ι → W)
 
-- Basis.constr：指定基向量的像，构造线性映射
#check (B.constr K : (ι → W) ≃ₗ[K] (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

10.4.3 线性映射的矩阵表示

variable {ι' : Type*} (B' : Basis ι' K W)
       [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι']
 
open LinearMap Matrix
 
-- 线性映射 → 矩阵
toMatrix B B' : (V →ₗ[K] W) ≃ₗ[K] Matrix ι' ι K
 
-- 矩阵乘法对应映射复合
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

toMatrix 是代数同态

toMatrix_comp：矩阵表示保持复合 toMatrix_id：恒等映射的矩阵是单位矩阵 Matrix.det_mul：行列式保持乘法

行列式与基无关：

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  -- P * M = M' * P，取行列式

10.4.4 维数

有限维：

#check (Module.finrank K V : ℕ)
 
-- 零维对应无限维（类似除零得零的设计）
 
-- 典型例子
example (n : ℕ) : Module.finrank K (Fin n → K) = n := Module.finrank_fin_fun K
example : Module.finrank ℂ ℂ = 1 := Module.finrank_self ℂ
example : Module.finrank ℝ ℂ = 2 := Complex.finrank_real_complex
 
-- 有限维假设
example [FiniteDimensional K V] : 0 < Module.finrank K V ↔ Nontrivial V :=
  Module.finrank_pos_iff

反向使用 finrank_pos_iff
Module.finrank_pos_iff 没有显式参数 K。反向使用时 Lean 猜不到域，需要用命名参数：
apply (Module.finrank_pos_iff (R := K)).1

维数公式：

example (E F : Submodule K V) [FiniteDimensional K V] :
    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 (E : Submodule K V) [FiniteDimensional K V] : finrank K E ≤ finrank K V :=
  Submodule.finrank_le E

无限维：用基数表示维数：

#check Module.rank K V  -- Cardinal.{u}
 
-- 两个基的索引类型基数相同
universe 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'
 
-- 有限维时 finrank 与 rank 一致
example [FiniteDimensional K V] : (Module.finrank K V : Cardinal) = Module.rank K V :=
  Module.finrank_eq_rank K V

宇宙层级

Cardinal.{u} 活在 Type (u+1)。不同宇宙的基数不能直接比较，需要用 Cardinal.lift。

本章核心概念总结

概念	符号/类型	关键操作
向量空间	`[Module K V]`	`•`, `smul_add`, `add_smul`
线性映射	`V →ₗ[K] W`	`map_add`, `map_smul`, `∘ₗ`
线性同构	`V ≃ₗ[K] W`	`f.symm`, `f ≪≫ₗ g`
子空间	`Submodule K V`	`⊓`, `⊔`, `⊤`, `⊥`, `span`
推前/拉回	`map`, `comap`	`ker`, `range`
商空间	`V ⧸ E`	`E.mkQ`, `E.liftQ`
自同态	`End K V`	`*`, `aeval`, `eigenspace`
矩阵	`Matrix m n α`	`!![...]`, `ᵥ`, `ᵥ`, `ᵀ`, `det`
基	`Basis ι K V`	`B.repr`, `B.constr`, `sum_repr`
矩阵表示	`toMatrix`	`toMatrix_mulVec_repr`
有限维数	`Module.finrank K V`	`finrank_fin_fun`, `finrank_self`
无限维数	`Module.rank K V`	`mk_eq_mk_of_basis`

关键学习策略

1. 线性映射构造模板

example : V →ₗ[K] W where
  toFun v := ...
  map_add' _ _ := ...
  map_smul' _ _ := ...

2. 子空间构造模板

def mySubspace : Submodule K V where
  carrier := {v : V | P v}
  zero_mem' := by ...
  add_mem' := by ...
  smul_mem' := by ...

3. 基的构造模板

-- 方式1：从同构
example (f : V ≃ₗ[K] (ι →₀ K)) : Basis ι K V := Basis.ofRepr f
 
-- 方式2：从线性无关+张成
noncomputable example (b : ι → V)
    (indep : LinearIndependent K b)
    (spans : ∀ v, v ∈ Submodule.span K (Set.range b)) : Basis ι K V :=
  Basis.mk indep (fun v _ ↦ spans v)

4. 证明向量相等 = ext + 字段证明

example (v w : V) (B : Basis ι K V) (h : ∀ i, B.repr v i = B.repr w i) : v = w := by
  rw [← B.sum_repr v, ← B.sum_repr w]
  congr
  funext i
  exact h i

预告：第11章会学到什么

第11章进入拓扑学：

滤子（Filter）和极限
度量空间（MetricSpace）
拓扑空间（TopologicalSpace）
连续映射

自测问题

为什么 Module K V 和 AddCommGroup V 要分开写？

线性映射复合用什么符号？为什么不能直接用 ∘？

Submodule K V 的 ⊔ 和集合的 ∪ 有什么区别？

Finsupp.linearCombination 的作用是什么？

toMatrix B B' φ 中矩阵的行列分别对应什么？

Module.finrank 对无限维空间返回什么？

伴读文档 - 第10章完

我的博客

探索

Ch10 线性代数 - 深度伴读

第10章线性代数 - 深度伴读

10.1 向量空间与线性映射

10.1.1 向量空间

10.1.2 线性映射

10.1.3 直和与直积

10.2 子空间与商空间

10.2.1 子空间

10.2.2 完备格结构

10.2.3 由集合生成的子空间

10.2.4 推前与拉回

10.2.5 商空间

10.3 自同态

10.3.1 基本定义

10.3.2 核引理（重要练习）

10.3.3 特征值与特征空间

10.3.4 极小多项式与 Cayley-Hamilton

10.4 矩阵、基与维数

10.4.1 矩阵

10.4.2 基

10.4.3 线性映射的矩阵表示

10.4.4 维数

本章核心概念总结

关键学习策略

1. 线性映射构造模板

2. 子空间构造模板

3. 基的构造模板

4. 证明向量相等 = ext + 字段证明

预告：第11章会学到什么

关系图谱

目录

反向链接

我的博客

探索

Ch10 线性代数 - 深度伴读

第10章 线性代数 - 深度伴读

10.1 向量空间与线性映射

10.1.1 向量空间

10.1.2 线性映射

10.1.3 直和与直积

10.2 子空间与商空间

10.2.1 子空间

10.2.2 完备格结构

10.2.3 由集合生成的子空间

10.2.4 推前与拉回

10.2.5 商空间

10.3 自同态

10.3.1 基本定义

10.3.2 核引理（重要练习）

10.3.3 特征值与特征空间

10.3.4 极小多项式与 Cayley-Hamilton

10.4 矩阵、基与维数

10.4.1 矩阵

10.4.2 基

10.4.3 线性映射的矩阵表示

10.4.4 维数

本章核心概念总结

关键学习策略

1. 线性映射构造模板

2. 子空间构造模板

3. 基的构造模板

4. 证明向量相等 = ext + 字段证明

预告：第11章会学到什么

关系图谱

目录

反向链接

第10章线性代数 - 深度伴读