第9章群与环 - 深度伴读

本章定位

本章应用第7-8章的层级概念，深入使用 Mathlib 的群论和环论库。重点：

群论：幺半群、群、子群、商群、群作用、Lagrange/Sylow 定理

环论：环、理想、商环、中国剩余定理、代数与多项式

本章内容量是前几章的总和，建议分多次学习。

9.1 Monoids and Groups

核心洞见

Monoid 是 Group 和 Ring 的乘法结构的共同抽象。Mathlib 中很多引理先在 Monoid 层面证明，自动适用于群和环。

9.1.1 Monoids and their morphisms

-- Monoid：乘法 + 结合律 + 单位元
example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x
 
-- 加法版本：AddMonoid（加法幺半群）
example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y

为什么需要 Monoid？

抽象代数课程通常从群开始，但环的乘法不构成群（0不可逆）。Monoid 是统一处理群乘法和环乘法的中间层。

Monoid 同态：

-- M →* N：乘法幺半群同态
example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) :
    f (x * y) = f x * f y := f.map_mul x y
 
-- M →+ N：加法幺半群同态
example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 := f.map_zero

bundled 映射不能用普通函数复合
用 g.comp f 而不是 g ∘ f：
example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
    (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f

9.1.2 Groups and their morphisms

-- Group：Monoid + 逆元
example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x
 
-- group tactic：自动证明群恒等式
example {G : Type*} [Group G] (x y z : G) :
    x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by group
 
-- abel tactic：加法交换群
example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by abel

group / abel tactic 的作用域

group：任何在任意群中成立的等式（等价于自由群中的等式）

abel：任何在任意加法交换群中成立的等式

群同态自动保持逆元：

example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ := f.map_inv x

从函数构造群同态（省掉证明 f 1 = 1 的步骤）：

example {G H : Type*} [Group G] [Group H] (f : G → H)
    (h : ∀ x y, f (x * y) = f x * f y) : G →* H :=
  MonoidHom.mk' f h

群同构 ≃*：

example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
    f.trans f.symm = MulEquiv.refl G := f.self_trans_symm
 
-- 从双射同态构造同构（noncomputable）
noncomputable example {G H : Type*} [Group G] [Group H]
    (f : G →* H) (h : Function.Bijective f) : G ≃* H :=
  MulEquiv.ofBijective f h

9.1.3 Subgroups

example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) :
    x * y ∈ H := H.mul_mem hx hy
 
example {G : Type*} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) :
    x⁻¹ ∈ H := H.inv_mem hx

Subgroup G 是类型，不是谓词

Subgroup G 是类型，不是 Set G → Prop。它带有 coercion 到 Set G。

构造子群：以 ℚ 中的 ℤ 为例

example : AddSubgroup ℚ where
  carrier := Set.range ((↑) : ℤ → ℚ)   -- ℤ 嵌入 ℚ 的像
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m; simp
  zero_mem' := by use 0; simp
  neg_mem' := by
    rintro _ ⟨n, rfl⟩
    use -n; simp

rintro + use + simp 模式

这是 Mathlib 中构造子结构的经典模式：

rintro 引入假设和存在性

use 提供存在见证

simp 简化证明

子群继承群结构：

example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance
-- 等价于：
example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance

子群构成完备格：

-- ⊓ = 交集（子群的交仍是子群）
example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl
 
-- ⊔ = 生成的子群（不是并集！）
example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by
  rw [Subgroup.sup_eq_closure]
 
-- ⊤ = 整个群
example {G : Type*} [Group G] (x : G) : x ∈ (⊤ : Subgroup G) := trivial
 
-- ⊥ = 平凡子群 {1}
example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot

并集不是子群

子群的并集一般不是子群。用 H ⊔ H' 表示”由 H ∪ H’ 生成的子群”。

共轭子群（练习）：

def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where
  carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
  one_mem' := by dsimp; use 1; simp [H.one_mem]
  inv_mem' := by
    dsimp
    rintro _ ⟨h, hh, rfl⟩
    use h⁻¹; constructor
    · exact H.inv_mem hh
    · simp [mul_assoc]
  mul_mem' := by
    dsimp
    rintro _ _ ⟨h₁, hh₁, rfl⟩ ⟨h₂, hh₂, rfl⟩
    use h₁ * h₂
    constructor
    · exact H.mul_mem hh₁ hh₂
    · simp [mul_assoc]

同态映射子群：

-- map = 推前（像）
example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
  Subgroup.map f G'
 
-- comap = 拉回（原像）
example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
  Subgroup.comap f H'
 
-- 核和像
example {G H : Type*} [Group G] [Group H] (f : G →* H) (g : G) :
    g ∈ MonoidHom.ker f ↔ f g = 1 := f.mem_ker
 
example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : H) :
    h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h := f.mem_range

经典定理：

open scoped Classical
 
-- Lagrange 定理：子群的阶整除群的阶
example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G :=
  ⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩
 
-- Sylow 第一定理：p^n 阶子群存在
example {G : Type*} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n :=
  Sylow.exists_subgroup_card_pow_prime p hdvd

open scoped Classical

允许使用非构造性逻辑（如选择公理），这是处理有限群时常用的。

9.1.4 Concrete groups

置换群：

open Equiv
 
-- 对称群 𝔖_n = Perm (Fin n)
example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
  Perm.closure_isCycle
 
-- c[1, 2, 3] 表示循环置换：1↦2, 2↦3, 3↦1，其余不动
-- 计算具体置换乘积
#simp [mul_assoc] c[1, 2, 3] * c[2, 3, 4]

自由群：

-- 自由群 FreeGroup α，包含映射 FreeGroup.of
inductive S | a | b | c
open S
 
def myElement : FreeGroup S := (.of a) * (.of b)⁻¹
 
-- 万有性质：FreeGroup.lift
-- 从 FreeGroup S 到 Perm (Fin 5) 的同态
 
def myMorphism : FreeGroup S →* Perm (Fin 5) :=
  FreeGroup.lift fun | .a => c[1, 2, 3]
                     | .b => c[2, 3, 1]
                     | .c => c[2, 3]

表现群（Presented Group）：

-- 定义一个关系集合（自由群的子集）
-- 生成元 () 满足 ()^3 = 1，即 ℤ/3ℤ
def myGroup := PresentedGroup {.of () ^ 3} deriving Group
 
-- 万有性质：发送关系到目标群的单位元
def myMap : Unit → Perm (Fin 5)
| () => c[1, 2, 3]
 
lemma compat_myMap :
    ∀ r ∈ ({.of () ^ 3} : Set (FreeGroup Unit)), FreeGroup.lift myMap r = 1 := by
  rintro _ rfl
  simp; decide
 
def myNewMorphism : myGroup →* Perm (Fin 5) := PresentedGroup.toGroup compat_myMap

9.1.5 Group actions

群作用 = 群到置换群的同态，但用类型类包装：

-- g • x：群元素 g 作用在 x 上
example {G X : Type*} [Group G] [MulAction G X] (g g': G) (x : X) :
    g • (g' • x) = (g * g') • x := (mul_smul g g' x).symm
 
-- 加法群作用（用于仿射空间）
example {G X : Type*} [AddGroup G] [AddAction G X] (g g' : G) (x : X) :
    g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x := (add_vadd g g' x).symm

轨道-稳定子定理：

-- 轨道与稳定子的商双射
example {G X : Type*} [Group G] [MulAction G X] (x : X) :
    orbit G x ≃ G ⧸ stabilizer G x :=
  MulAction.orbitEquivQuotientStabilizer G x
 
-- 子群 H 的陪集分解
def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
  Equiv.Perm.subgroupOfMulAction G G

群作用的练习模式

定义 smul（作用）

证明 one_smul（单位元作用不变）

证明 mul_smul（作用相容于乘法）

instance : MulAction G (Subgroup G) where
  smul := conjugate
  one_smul := by sorry    -- 1 • H = H
  mul_smul := by sorry    -- (gh) • H = g • (h • H)

9.1.6 Quotient groups

商群 G ⧸ N 需要 N 是正规子群 [N.Normal]：

example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] : Group (G ⧸ H) := inferInstance
 
-- 商映射
example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] : G →* G ⧸ N :=
  QuotientGroup.mk' N

万有性质：

-- 核包含 N 的同态可下降到商
example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] {M : Type*}
    [Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
  QuotientGroup.lift N φ h
 
-- 第一同构定理
example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
    G ⧸ MonoidHom.ker φ ≃* MonoidHom.range φ :=
  QuotientGroup.quotientKerEquivRange φ

G ⧸ N 依赖于 N 的定义
两个定义上相等的正规子群可能产生不同的商类型。但万有性质给出同构：
example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal]
    (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h

9.2 Rings

9.2.1 Rings, units, morphisms and subrings

-- ring tactic 适用于任何 CommSemiring
example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

单位元（可逆元素）：

-- Mˣ = Units M：可逆元素类型（bundled with its inverse）
example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x
 
-- IsUnit x：x 是可逆的（Prop）
example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x

Units M 自动构成群

example {M : Type*} [Monoid M] : Group Mˣ := inferInstance

环同态 R →+* S：

example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) :
    f (x + y) = f x + f y := f.map_add x y
 
-- 单位元映射到单位元
example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ := Units.map f

9.2.2 Ideals and quotients

理想 = 作为 R-模的子模：

example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
  Ideal.Quotient.mk I
 
-- a ∈ I ↔ [a] = 0
example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
    Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
  Ideal.Quotient.eq_zero_iff_mem

匿名投影符号的陷阱

I.Quotient.mk 解析为 (Ideal.Quotient I).mk，但 Ideal.Quotient 本身不存在。必须用 Ideal.Quotient.mk I。

理想运算：

variable {R : Type*} [CommRing R] {I J : Ideal R}
 
-- I + J = I ⊔ J（作为子模的和）
example : I + J = I ⊔ J := rfl
example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by simp [Submodule.mem_sup]
 
-- I * J：理想的乘积
example : I * J ≤ J := Ideal.mul_le_left
example : I * J ≤ I := Ideal.mul_le_right
example : I * J ≤ I ⊓ J := Ideal.mul_le_inf

中国剩余定理（重要练习）：

-- ker_Pi_Quotient_mk：ker (Π i, R ⧸ I i) = ⨅ i, I i
-- 即：对所有 i 都有 a ≡ 0 (mod I i) ↔ a ∈ ⋂ i, I i
 
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  Ideal.Quotient.lift (⨅ i, I i)
    (Pi.ringHom fun i ↦ Ideal.Quotient.mk (I i))
    (by rw [ker_Pi_Quotient_mk]; rfl)
 
-- 关键引理：单射性来自 ker = 0
lemma chineseMap_inj (I : ι → Ideal R) : Injective (chineseMap I) := by
  rw [injective_lift_iff]    -- 提升映射单射 ↔ 核条件满足
  rw [ker_Pi_Quotient_mk]    -- 核 = ⨅ i, I i，正好是提升的模
  rfl
 
-- 互素 ⇒ 满射
lemma chineseMap_surj [Fintype ι] {I : ι → Ideal R}
    (hI : ∀ i j, i ≠ j → IsCoprime (I i) (I j)) : Surjective (chineseMap I) := by
  classical
  intro g
  choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
  -- 构造中国剩余定理中的 e_i：e_i ≡ 1 (mod I_i)，e_i ≡ 0 (mod I_j, j≠i)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by sorry
  choose e he using key
  use mk _ (∑ i, f i * e i)
  sorry

IsCoprime 的等价形式

IsCoprime I J

I + J = ⊤

∃ a ∈ I, ∃ b ∈ J, a + b = 1

I ⊔ J = ⊤

9.2.3 Algebras and polynomials

代数：环 A 配备 R-代数结构 Algebra R A：

-- structureMap：R → A
example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r : R) : A :=
  algebraMap R A r
 
-- 标量乘法 r • a = algebraMap R A r * a
example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
    (r + r') • a = r • a + r' • a := add_smul r r' a

多项式 R[X]：

open Polynomial
 
-- 不定元 X
example {R : Type*} [CommRing R] : R[X] := X
 
-- 常数多项式 C r
example {R : Type*} [CommRing R] (r : R) := X - C r
 
-- C 是环同态，可用 map_zero, map_mul, map_pow
example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
  rw [C.map_pow]
  ring

多项式求值的区别

函数输入输出用途
P.eval r r : R R 在系数环中求值
aeval a P a : A（R-代数） A 在任何 R-代数中求值
eval₂ f s f : R →+* S, s : S S 沿环同态求值

函数	输入	输出	用途
`P.eval r`	r : R	R	在系数环中求值
`aeval a P`	a : A（R-代数）	A	在任何 R-代数中求值
`eval₂ f s`	f : R →+* S, s : S	S	沿环同态求值

-- eval：在 R 中求值
example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp
 
-- aeval：在任何 R-代数中求值
example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp
 
-- eval₂：沿环同态求值
example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofRealHom Complex.I = 0 := by simp

多项式的次数：

-- natDegree：零多项式的次数为 0
-- degree：零多项式的次数为 ⊥（WithBot ℕ）
 
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    degree (p * q) = degree p + degree q := Polynomial.degree_mul
 
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} (hp : p ≠ 0) (hq : q ≠ 0) :
    natDegree (p * q) = natDegree p + natDegree q := Polynomial.natDegree_mul hp hq

WithBot ℕ 的陷阱

⊥ + 0 = ⊥（吸收元），但 ⊥ * 0 = 0（不吸收）！

根：

-- roots：返回 Multiset（零多项式返回空集）
example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
  roots_X_sub_C r
 
-- aroots：在代数闭包中求根
example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
  suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by sorry
  sorry

本章核心概念总结

概念	符号/类型	关键操作
Monoid	`[Monoid M]`	`*`, `1`, `group` tactic
Group	`[Group G]`	`⁻¹`, `group` tactic
群同态	`G →* H`	`f.map_mul`, `f.map_inv`
群同构	`G ≃* H`	`f.symm`, `f.trans`
子群	`Subgroup G`	`H ⊓ H'`, `H ⊔ H'`, `⊤`, `⊥`
核/像	`ker f`, `range f`	`f.mem_ker`
商群	`G ⧸ N`	`QuotientGroup.mk'`, `lift`
环	`[CommRing R]`	`ring` tactic
理想	`Ideal R`	`I + J`, `I * J`, `I ⊓ J`
商环	`R ⧸ I`	`Ideal.Quotient.mk`
代数	`[Algebra R A]`	`algebraMap`, `aeval`
多项式	`R[X]`	`C`, `X`, `eval`, `aeval`

关键学习策略

1. 子群构造模板

def mySubgroup : Subgroup G where
  carrier := {x : G | P x}
  one_mem' := by ...
  inv_mem' := by ...
  mul_mem' := by ...

2. 商群使用模板

-- 1. 确保子群正规（或假设 [N.Normal]）
-- 2. 定义商映射
-- 3. 用 lift 下降同态
-- 4. 用 quotientKerEquivRange 得第一同构定理

3. 中国剩余定理证明策略

-- 1. 构造 chineseMap
-- 2. 证单射（核 = 0）
-- 3. 证满射（构造 e_i 用 IsCoprime）
-- 4. 组合为 Equiv.ofBijective

预告：第10章会学到什么

第10章进入线性代数：

Module K V：向量空间（域上的模）
V →ₗ[K] W：线性映射
Submodule K V：子空间
V ⧸ E：商空间
Basis ι K V：基
矩阵和 toMatrix

自测问题

为什么需要 Monoid？它和 Group 有什么区别？

Subgroup G 为什么设为类型而不是谓词？

商群 G ⧸ N 需要什么条件？

aeval 和 eval 有什么区别？

理想乘积 I * J 和交集 I ⊓ J 有什么关系？

伴读文档 - 第9章完

我的博客

探索

Ch9 群与环 - 深度伴读

第9章群与环 - 深度伴读

9.1 Monoids and Groups

9.1.1 Monoids and their morphisms

9.1.2 Groups and their morphisms

9.1.3 Subgroups

9.1.4 Concrete groups

9.1.5 Group actions

9.1.6 Quotient groups

9.2 Rings

9.2.1 Rings, units, morphisms and subrings

9.2.2 Ideals and quotients

9.2.3 Algebras and polynomials

本章核心概念总结

关键学习策略

1. 子群构造模板

2. 商群使用模板

3. 中国剩余定理证明策略

预告：第10章会学到什么

关系图谱

目录

反向链接

我的博客

探索

Ch9 群与环 - 深度伴读

第9章 群与环 - 深度伴读

9.1 Monoids and Groups

9.1.1 Monoids and their morphisms

9.1.2 Groups and their morphisms

9.1.3 Subgroups

9.1.4 Concrete groups

9.1.5 Group actions

9.1.6 Quotient groups

9.2 Rings

9.2.1 Rings, units, morphisms and subrings

9.2.2 Ideals and quotients

9.2.3 Algebras and polynomials

本章核心概念总结

关键学习策略

1. 子群构造模板

2. 商群使用模板

3. 中国剩余定理证明策略

预告：第10章会学到什么

关系图谱

目录

反向链接

第9章群与环 - 深度伴读