8. 群与环

在 Section 2.2 中，我们已经学习了如何推导群和环中的运算规则。而在稍后的 Section 6.2 中，我们探讨了定义抽象代数结构的方法，例如群的结构， 以及像高斯整环这样的具体实例。Chapter 7 详细说明了 Mathlib 是如何处理这些抽象结构的层级关系的。

本章将更深入地探讨群和环的相关内容。由于 Mathlib 仍在不断发展，我们无法全面覆盖所有内容， 但会提供使用相关库的切入点，并展示如何运用其核心概念。虽然本章的部分内容与 Chapter 7 有所重叠， 但我们的重点在于指导如何使用 Mathlib，而非分析其设计背后的理念。因此，为了更好地理解本章的部分示例，可能需要回顾 Chapter 7。

8.1. 幺半群与群

8.1.1. 幺半群和同态

抽象代数课程通常从群开始，逐步深入到环、域直至向量空间。这种教学顺序常会导致讨论环上的乘法等非群结构运算时出现不必要的曲折：许多群定理证明的方法同样适用，但我们却要重新证明。 一般来说，当你用书本学习数学时，多数作者用一行 “以下留作习题” 化解此窘境。不过，在 Lean 中，我们有另一种虽然不那么方便，但更安全，更适于形式化的方法：引入幺半群 (monoid)。

类型 M 上的 幺半群 是一个内部具有结合律和单位元的复合法则 (composition law)。幺半群引入的初衷是同时描述群和环的乘法结构。一些自然的例子如：自然数与加法构成一个幺半群。

从实用的角度而言，你几乎可以忘记 Mathlib 中的幺半群。但了解其存在是有益的，否则在寻找那些实际上并不需要元素可逆的引理时，你可能忽略它们在幺半群而非群的文件中。

类型 M 上的幺半群被写作 Monoid M. 函数 Monoid 是一个类型类，所以通常作为隐式实例参数而出现。（即在方括号中） Monoid 默认用乘号作运算符号。如需使用加号，可以使用 AddMonoid。 若需满足交换律，可使用 CommMonoid.

example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x

example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y

注意：虽然库中确实定义了 AddMonoid，但将加号用于非交换的运算可能会导致混淆。

幺半群 M 与 N 间的同态的类型称为 MonoidHom M N，可写作 M →* N. 在将一个同态作用于类型 M 的元素时，Lean 将视其为一个由 M 到 N 的函数。相应的加法版本被称为 AddMonoidHom, 写作 M →+ N. 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

example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
  f.map_zero

同态其实是一系列映射, 即：同态映射本身和它的一些性质。 Section 7.2 中对这样的系列映射有解释。 现在，我们发现这也产生了些不妙的效果：我们无法使用常规的函数复合来复合两个映射。对此，有 MonoidHom.comp 和 AddMonoidHom.comp.

example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
    (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f

8.1.2. 群和同态

对于群，我们有更多可以探讨的。群，就是幺半群加上每一个元素都有逆元的性质。

example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x

正如之前我们看到的 ring 策略，我们有 group 策略用来证明所有群所共同满足的恒等式。 (即自由群所满足的恒等式)

example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
  group

对满足交换律的群，还有 abel 策略.

example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
  abel

有趣的是，群同态所需满足的实际上与幺半群别无二致。所以我们之前的例子可以照搬过来。

example {G H : Type*} [Group G] [Group H] (x y : G) (f : G →* H) : f (x * y) = f x * f y :=
  f.map_mul x y

当然也有点新性质：

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

你也许会担心构造一个群同态需要枉费些不必要的工夫：幺半群同态的定义需要映射保持幺元，可这是群的情况下由第一条保持运算的性质就能自动得到的。虽然在实际中多做这一步并不困难，但我们可以避免它。接下来的函数可以由保持运算的群间映射给出群同态.

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

同样对于群（幺半群）同构，我们有类型 MulEquiv , 记为 ≃* (对应加号版本 AddEquiv 记为 ≃+).

f : G ≃* H 的逆是 MulEquiv.symm f : H ≃* G, f 和 g 的复合是 MulEquiv.trans f g, G 到自身的恒等同构 M̀ulEquiv.refl G.

使用匿名投影子记号, 前两个可对应写作 f.symm 和 f.trans g. 这些类型的元素将在必要时自动转换为同态或函数.

example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
    f.trans f.symm = MulEquiv.refl G :=
  f.self_trans_symm

你可以用 MulEquiv.ofBijective 从一个也是双射的同态构造同构. 同时这样做会使逆映射被标记为不可计算的 (noncomputable).

noncomputable example {G H : Type*} [Group G] [Group H]
    (f : G →* H) (h : Function.Bijective f) :
    G ≃* H :=
  MulEquiv.ofBijective f h

8.1.3. 子群

就像群同态是一系列映射一样，G 的子群也是一个由类型 G 的集合和相应的封闭性质所共同构成结构。

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 是 G 的子群的类型，而不是对一个 Set G 中元素 H 的附加的断言 IsSubgroup H. Subgroup G 类型已经被赋予了到 Set G 的类型转换和一个与 G 间的包含关系的判断。 参见 Section 7.3 以了解这是为何要以及如何完成的。

当然，两个子群相同当且仅当它们包含的元素完全相同。这一事实被注册到了 ext 策略, 所以你可以像证明两个集合相等一样来证明两个子群相等。

当我们论证类似 ℤ 是 ℚ 的一个加性子群这样的命题时, 我们真正想要的其实相当于是构造一个 AddSubgroup ℚ 类型的项，该项到 Set ℚ 的投影为 ℤ，或者更精确的说，ℤ 在 ℚ 中的像.

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

通过使用类型类，Mathlib 知道群的子群继承了群结构。

example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance

这一个例子隐含了一些信息. 对象 H 并不是一个类型, 但 Lean 通过将其解释为 G 的子类型自动将其转换为了一个类型. 以上例子还可以用更清晰的方式来表述:

example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance

使用类型``Subgroup G`` 而不是断言 IsSubgroup : Set G → Prop 的一个重要优势在于可以为 Subgroup G 轻松地赋予额外的结构. 重要的是, 它具有对于包含关系的完备格结构 (lattice structure). 例如, 相较于用额外的引理来说明两个 G 的子群的交仍然是一个子群, 我们可以使用格运算符 ⊓ 直接构造出这个交集构成的子群. 我们可以将有关格的任意引理应用到这样的构造上.

现在我们来检验, 两个子群的下确界导出的集合, 从定义上来说, 确实是它们的交集.

example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl

为实际上给出了集合交集的运算使用另一个记号可能有些奇怪, 但要知道，这样的对应关系在上确界与并集运算之间不再成立. 因为一般来说, 子群的并不再构成一个子群. 我们需要的是这样的并生成的子群, 这可以使用 Subgroup.closure 来得到.

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]

另一个微妙的地方在于 G 本身并不具有类型 Subgroup G, 所以我们需要一种方式来将 G 视作它自身的子群. 这同样由格结构来证明: 全集构成的子群是格中的最大元.

example {G : Type*} [Group G] (x : G) : x ∈ (⊤ : Subgroup G) := trivial

类似的，格中的最小元是只包含有单位元的子群.

example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot

作为操作群与子群的练习，你可以定义一个子群与环境群中的元素得到的共轭子群.

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
    sorry
  inv_mem' := by
    dsimp
    sorry
  mul_mem' := by
    dsimp
    sorry

将前两个主题结合在一个, 我们就可以使用群同态来“前推” (push forward) 或“拉回” (pull back) 子群. Mathlib 中的命名习惯是将这两个操作称为 map 和 comap. 它们并不是常见的数学名词, 但它们的优势在于较 “pushforward” 和 “direct image” 更为简洁.

example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
  Subgroup.map f G'

example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
  Subgroup.comap f H'

#check Subgroup.mem_map
#check Subgroup.mem_comap

特别的, 最小子群（即只含单位元的群）在同态 f 下的前像构成一个被称为同态 f 的 核 的子群, 而 f 的值域同样也是一个子群.

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

作为操作群同态和子群的练习, 我们来证明一些初等性质. Mathlib 已经证明了它们, 所以如果你想真正锻炼自己，最好不要依赖于 exact?。

section exercises
variable {G H : Type*} [Group G] [Group H]

open Subgroup

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  sorry

example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
  sorry

variable {K : Type*} [Group K]

-- 记得你可以用 `ext` 策略证明子群的相等性.
example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
    comap (ψ.comp φ) U = comap φ (comap ψ U) := by
  sorry

-- 将一个子群先后通过两个群同态 “前推” 相当于通过这些同态的复合 “前推” .
example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
    map (ψ.comp φ) S = map ψ (S.map φ) := by
  sorry

end exercises

让我们用两个非常经典的例子来结束对 Mathlib 中子群的介绍. 拉格朗日定理 (Lagrange theorem) 说明了有限群的子群的阶可以整除该群的阶. 西罗第一定理 (Sylow’s first theorem)，是拉格朗日定理的一个著名部分逆定理.

虽然 Mathlib 的这一部分是部分为了允许计算而设置的，但我们可以通过以下的 open scoped 命令告诉 Lean 使用非构造性逻辑。

open scoped Classical


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⟩

open Subgroup

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

接下来的两个练习推导出拉格朗日引理的一个推论。（Mathlib 也已经有证明，所以也不要太快地使用 exact?）

lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} :
    H = ⊥ ↔ Nat.card H = 1 := by
  suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
    simpa [eq_bot_iff_forall, Nat.card_eq_one_iff_exists]
  sorry

#check card_dvd_of_le

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  sorry

8.1.4. 具体群

在 Mathlib 中，也可以操作具体的群，尽管这通常比处理抽象理论更为复杂。 例如, 对任意一个类型 X, X 的置换群为 Equiv.Perm X. 特别的，对称群 \(\mathfrak{S}_n\) 是 Equiv.Perm (Fin n). 你也可以论述关于这些群的抽象事实, 比如 Equiv.Perm X 在 X 有限时 是由轮换生成的.

open Equiv

example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
  Perm.closure_isCycle

可以完全具体化并计算轮换的实际乘积. 下面使用 #simp 命令, 其调用 simp 策略作用于表达式. 记号 c[] 用于表示轮换表示下的置换. 本例中是 ℕ 上的置换. 也可以在第一个元素上用 (1 : Fin 5) 这样的类型标注使其在 Perm (Fin 5) 上计算.

#simp [mul_assoc] c[1, 2, 3] * c[2, 3, 4]

另一种处理具体群的方式是使用自由群及其相关表示. 类型 α 上的自由群是一个 FreeGroup α , 对应包含映射为 FreeGroup.of : α → FreeGroup α. 例如，可以定义类型 S ，其中有三个元素 a, b 和 c, 这些元素可以构成自由群中的元素 ab⁻¹.

section FreeGroup

inductive S | a | b | c

open S

def myElement : FreeGroup S := (.of a) * (.of b)⁻¹

我们给出了预期的类型，所以 Lean 能推断出 .of 代表着 FreeGroup.of.

自由群的整体性质体现在等价性 FreeGroup.lift 中. 例如，可以定义 FreeGroup S 到 Perm (Fin 5) 的群同态: 映射 a 到 c[1, 2, 3], b 到 c[2, 3, 1], c 到 c[2, 3],

def myMorphism : FreeGroup S →* Perm (Fin 5) :=
  FreeGroup.lift fun | .a => c[1, 2, 3]
                     | .b => c[2, 3, 1]
                     | .c => c[2, 3]

最后一个例子, 让我们通过定义一个元素立方为单位来生成一个群 (也即同构于 \(\mathbb{Z}/3\)) 并构造从其到 Perm (Fin 5) 的态射.

Unit 类型只有一个元素，表示为 (). 函数 PresentedGroup 接受一系列关系, (即一系列某个自由群中的元素), 并将这个自由群模去由这些关系(元素)生成的正规子群, 返回得到的商群. (在 Section 8.1.6 中将展示如何处理更一般的商关系) 为简化定义, 我们使用 deriving Group to 直接生成 myGroup 上的群实例.

def myGroup := PresentedGroup {.of () ^ 3} deriving Group

presented groups 的整体性质确保了可以由那些将关系元都映射到目标群的单位元的函数构造群同态. 我们只需要一个函数和其满足该性质的证明, 就能用 PresentedGroup.toGroup 得到所需的群态射.

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

end FreeGroup

8.1.5. 群作用

群作用是群论与其它数学相作用的一项重要方式. 群 G 在某类型 X 上的一个作用也正是 G 到 Equiv.Perm X 的一个态射. 所以某种意义上来说群作用已经为前文的讨论所涉及了. 不过我们并不想显式地给出这个态射; 它应该更多可能的由 Lean 自动推断得到. 对此, 我们有类型类 MulAction G X. 这种方式的缺点是, 当我们有同一个群在同一类型上的多个群作用时, 会产生一些曲折, 比如将定义携带不同类型类实例的同义类型.

实例化类型类之后，我们可以使用 g • x 表示群中的 g 作用在 点 x 上.

noncomputable section GroupActions

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

对应的加法版本为 AddAction, 记号是 +ᵥ. 仿射空间的定义中会用到这个实例.

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

底层的群态射为 MulAction.toPermHom.

open MulAction

example {G X : Type*} [Group G] [MulAction G X] : G →* Equiv.Perm X :=
  toPermHom G X

为了说明这一点，让我们看看如何将任意群 G 的 Cayley 同构嵌入定义为一个置换群，即 Perm G。

def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
  Equiv.Perm.subgroupOfMulAction G G

以下是这段话的翻译：

请注意，在上述定义之前，并不需要一定是群，而是可以是幺半群或者任何具有乘法操作的类型。

群的条件真正开始发挥作用是在我们需要将 X 分成轨道（orbits）时。对应于 X 的等价关系被称为 MulAction.orbitRel。 这个等价关系并没有被声明为一个全局实例。

example {G X : Type*} [Group G] [MulAction G X] : Setoid X := orbitRel G X

利用这一点，我们可以说明在群 G 的作用下，集合 X 被划分为多个轨道 (orbits) 。

更具体地说，我们得到一个集合 X 与一个依赖乘积类型 (dependent product) (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) 之间的双射, 其中, Quotient.out' ω 简单地选择一个元素，该元素映射到 ω。

请注意，该依赖积的元素是形如 ⟨ω, x⟩ 的对，其中 x 的类型 orbit G (Quotient.out' ω) 依赖于 ω。

example {G X : Type*} [Group G] [MulAction G X] :
    X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) :=
  MulAction.selfEquivSigmaOrbits G X

特别是，当 X 是有限集时，可以结合 Fintype.card_congr 和 Fintype.card_sigma 推导出 X 的基数等于其轨道 (orbits) 基数之和。

此外，这些轨道与 G 在稳定子 (stabilizers) 的左平移作用下的商集 (quotient) 一一对应 (存在双射关系)。 这种通过子群的左平移作用定义的商集通常使用符号 / 来表示，因此可以用以下简洁的表述来说明。

example {G X : Type*} [Group G] [MulAction G X] (x : X) :
    orbit G x ≃ G ⧸ stabilizer G x :=
  MulAction.orbitEquivQuotientStabilizer G x

将上述两个结果结合的一个重要特殊情况是当 X 是一个通过平移作用配备了一个子群 H 的群 G 。 在这种情况下，所有稳定子都是平凡的，因此每个轨道都与 H 一一对应，我们得到：

example {G : Type*} [Group G] (H : Subgroup G) : G ≃ (G ⧸ H) × H :=
  groupEquivQuotientProdSubgroup

这是我们前面看到的拉格朗日定理版本的概念变体。 请注意，这个版本并不假设有限性。

作为本节的练习，让我们使用前面练习中的 conjugate 定义，构建一个群对其子群通过共轭作用的群作用。

variable {G : Type*} [Group G]

lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
  sorry

instance : MulAction G (Subgroup G) where
  smul := conjugate
  one_smul := by
    sorry
  mul_smul := by
    sorry

end GroupActions

8.1.6. 商群

在上述关于子群作用于群的讨论中，我们看到了商 G ⧸ H 的出现。 一般来说，这只是一个类型。只有当 H 是正规子群时，它才能被赋予群结构，使得商映射是一个群态射（group morphism）（并且这种群结构是唯一的）。

正规性假设是一个类型类 Subgroup.Normal，因此类型类推断可以使用它来导出商上的群结构。

noncomputable section QuotientGroup

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
  QuotientGroup.mk' H

通过 QuotientGroup.lift 可以使用商群的整体性质： 当且仅当群态射 φ 的核包含 N 时，φ 可以下降为 G ⧸ 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

目标群被称为 M 这一事实表明，M 拥有幺半群结构就足够了。

一个重要的特殊情况是当 N = ker φ 时。在这种情况下，下降的态射是单射，并且我们得到一个从群到其像的群同构。这个结果通常被称为 第一同构定理。

example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
    G ⧸ MonoidHom.ker φ →* MonoidHom.range φ :=
  QuotientGroup.quotientKerEquivRange φ

将整体性质应用于一个态射 φ : G →* G' 与商群投影 Quotient.mk' N' 的组合时，我们也可以构造一个从 G ⧸ N 到 G' ⧸ N' 的态射。

对 φ 的条件通常表述为 “φ 应该将 N 映射到 N' 内部。” 但这相当于要求 φ 应该将 N' 拉回到 N 上，而后者的条件更便于处理，因为拉回（pullback）的定义不涉及存在量词。

example {G G': Type*} [Group G] [Group G']
    {N : Subgroup G} [N.Normal] {N' : Subgroup G'} [N'.Normal]
    {φ : G →* G'} (h : N ≤ Subgroup.comap φ N') : G ⧸ N →* G' ⧸ N':=
  QuotientGroup.map N N' φ h

需要注意的一个细微点是，类型 G ⧸ N 实际上依赖于 N``（在定义等同的范围内），因此证明两个正规子群 ``N 和 M 是相等的并不足以使相应的商群相等。然而，在这种情况下，整体性质确实给出了一个同构。

example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
    [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h

作为本节的最后一组练习，我们将证明：如果 H 和 K 是有限群 G 的不相交正规子群，且它们的基数的乘积等于 G 的基数，那么 G 同构于 H × K。请记住，这里的 “不相交” 意味着 H ⊓ K = ⊥。

我们从拉格朗日引理的一些操作开始，此时不假设子群是正规或不相交的。

section
variable {G : Type*} [Group G] {H K : Subgroup G}

open MonoidHom

#check Nat.card_pos -- 参数将从子群条件中隐式推导出
#check Subgroup.index_eq_card
#check Subgroup.index_mul_card
#check Nat.eq_of_mul_eq_mul_right

lemma aux_card_eq [Finite G] (h' : Nat.card G = Nat.card H * Nat.card K) :
    Nat.card (G ⧸ H) = Nat.card K := by
  sorry

从现在开始，我们假设我们的子群是正规且不相交的，并假设基数条件。现在，我们构造所需同构的第一个部分。

variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K)
  (h' : Nat.card G = Nat.card H * Nat.card K)

#check Nat.bijective_iff_injective_and_card
#check ker_eq_bot_iff
#check restrict
#check ker_restrict

def iso₁ [Fintype G] (h : Disjoint H K) (h' : Nat.card G = Nat.card H * Nat.card K) : K ≃* G ⧸ H := by
  sorry

现在我们可以定义第二个部分。 我们将需要 MonoidHom.prod，它可以根据从 G₀ 到 G₁ 和 G₂ 的态射构建一个从 G₀ 到 G₁ × G₂ 的态射。

def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
  sorry

再将这两部分结合起来.

#check MulEquiv.prodCongr

def finalIso : G ≃* H × K :=
  sorry

8.2. 环

8.2.1. 环、环上的单位元、态射和子环

类型 R 上环结构的类型是 Ring R。乘法交换的变体为 CommRing R。 我们已经看到，ring 策略会证明任何基于交换环公理的等式。

example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

更为奇特的变体不要求 R 上的加法形成群，而仅需是加法幺半群。对应的类型类是 Semiring R 和 CommSemiring R。

自然数类型是 CommSemiring R 的一个重要实例，任何以自然数为值的函数类型也是如此。 另一个重要的例子是环中的理想的类型，这将在下面讨论。

ring 策略的名称是双重误导性的，因为它假设了交换性，但也适用于半环。换句话说，它适用于任何 CommSemiring。

example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

还有一些环类和半环类的变体不假设乘法单位元的存在或乘法的结合性。我们在这里不讨论这些。

某些传统上在环论入门中教授的概念实际上是关于底层乘法幺半群的。 一个突出的例子是环的单位元的定义。每个（乘法）幺半群 M 都有一个谓词 IsUnit : M → Prop，用来断言存在双边逆元，一个类型 Units M 表示单位元，并用记号 Mˣ 表示，以及到 M 的强制转换。 类型 Units M 将一个可逆元素与其逆元以及确保它们彼此互为逆元的性质一起打包。 此实现细节主要与定义可计算函数相关。在大多数情况下，可以使用 IsUnit.unit {x : M} : IsUnit x → Mˣ 构造一个单位元。 在交换情况下，还可以使用 Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ 构造 x 作为单位元。

example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x

example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x

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

两个（半）环 R 和 S 之间环态射的类型是 RingHom R S，记号为 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

同构的变体是 RingEquiv，记号为 ≃+*。

与子幺半群和子群类似，环 R 的子环有一个类型 Subring R，但这个类型远不如子群类型有用，因为环不能通过子环进行商构造。

example {R : Type*} [Ring R] (S : Subring R) : Ring S := inferInstance

值得注意的是，RingHom.range 产生一个子环。

8.2.2. 理想与商

由于历史原因，Mathlib 仅为交换环提供了理想的理论。 （环库最初的开发是为了快速推进现代代数几何的基础。）因此，在本节中我们将讨论交换（半）环。 R 的理想被定义为将 R 视为 R-模的子模。模将在线性代数的章节中讨论，但这一实现细节基本上可以安全忽略，因为大多数（但不是全部）相关引理都已在理想的特殊背景中重新叙述。但是匿名投影记号并不总是像预期的那样工作。例如，不能将 Ideal.Quotient.mk I 替换为 I.Quotient.mk，因为下面的代码片段中有两个 .，因此它会被解析为 (Ideal.Quotient I).mk；但单独的 Ideal.Quotient 并不存在。

example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
  Ideal.Quotient.mk I

example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
    Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
  Ideal.Quotient.eq_zero_iff_mem

商环的整体性质是 Ideal.Quotient.lift。

example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S)
    (H : I ≤ RingHom.ker f) : R ⧸ I →+* S :=
  Ideal.Quotient.lift I f H

特别的，其导出了环的第一同构定理。

example {R S : Type*} [CommRing R] [CommRing S](f : R →+* S) :
    R ⧸ RingHom.ker f ≃+* f.range :=
  RingHom.quotientKerEquivRange f

理想在包含关系下形成一个完备格结构，同时也具有半环结构。这两个结构相互作用良好。

variable {R : Type*} [CommRing R] {I J : Ideal R}

example : I + J = I ⊔ J := rfl

example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by
  simp [Submodule.mem_sup]

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

可以使用环态射分别通过 Ideal.map 和 Ideal.comap 将理想前推（push forward）或拉回（pull back）。 通常情况下，后者更方便使用，因为它不涉及存在量词。这也解释了为何它被用来表达构造商环之间态射的条件。

example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S)
    (H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J :=
  Ideal.quotientMap J f H

一个需要注意的细微点是，类型 R ⧸ I 实际上依赖于 I``（在定义等同的范围内），因此证明两个理想 ``I 和 J 相等并不足以使相应的商环相等。然而，在这种情况下，整体性质确实提供了一个同构。

example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
  Ideal.quotEquivOfEq h

我们现在可以将中国剩余定理的同构作为一个示例呈现。请注意，索引下确界符号 ⨅ 与类型大乘积符号 Π 的区别。取决于你的字体，它们可能很难区分。

example {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] (f : ι → Ideal R)
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
  Ideal.quotientInfRingEquivPiQuotient f hf

初等版本的中国剩余定理（关于 ZMod 的表述）可以轻松地从前述定理推导出来：

open BigOperators PiNotation

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → (a i).Coprime (a j)) :
    ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
  ZMod.prodEquivPi a coprime

作为一系列练习，我们将在一般情况下重新证明中国剩余定理。

我们首先需要定义定理中出现的映射，作为一个环态射，利用商环的整体性质。

variable {ι R : Type*} [CommRing R]
open Ideal Quotient Function

#check Pi.ringHom
#check ker_Pi_Quotient_mk

/-- 从 ``R ⧸ ⨅ i, I i`` 到 ``Π i, R ⧸ I i`` 的同态映射，该映射在中国剩余定理中出现。 -/
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  sorry

确保以下两个引理可以通过 rfl 证明。

lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
  sorry

lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
    chineseMap I (mk _ x) i = mk (I i) x :=
  sorry

下一个引理证明了中国剩余定理的简单部分，对于理想族没有任何假设。该证明不到一行即可完成。

#check injective_lift_iff

lemma chineseMap_inj (I : ι → Ideal R) : Injective (chineseMap I) := by
  sorry

我们现在准备进入定理的核心部分，它将展示我们的 chineseMap 的满射性。 首先，我们需要了解几种表达互素性（也称为互为最大假设 co-maximality assumption ）的方法。以下仅需要使用前两种表达方式。

#check IsCoprime
#check isCoprime_iff_add
#check isCoprime_iff_exists
#check isCoprime_iff_sup_eq
#check isCoprime_iff_codisjoint

我们借此机会对 Finset 使用归纳法。以下列出了关于 Finset 的相关引理。 请记住，ring 策略适用于半环，并且环的理想构成一个半环。

#check Finset.mem_insert_of_mem
#check Finset.mem_insert_self

theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
  classical
  simp_rw [isCoprime_iff_add] at *
  induction s using Finset.induction with
  | empty =>
      simp
  | @insert i s _ hs =>
      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
      set K := ⨅ j ∈ s, J j
      calc
        1 = I + K                  := sorry
        _ = I + K * (I + J i)      := sorry
        _ = (1 + K) * I + K * J i  := sorry
        _ ≤ I + K ⊓ J i            := sorry

我们现在可以证明在中国剩余定理中出现的映射的满射性。

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)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      sorry
    sorry
  choose e he using key
  use mk _ (∑ i, f i * e i)
  sorry

将这些部分结合起来：

noncomputable def chineseIso [Fintype ι] (f : ι → Ideal R)
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
  { Equiv.ofBijective _ ⟨chineseMap_inj f, chineseMap_surj hf⟩,
    chineseMap f with }

8.2.3. 代数与多项式

给定一个交换（半）环 R，一个 R 上的 代数 (algebra) R 是一个半环 A，其配备了一个环态射，其像与 A 的每个元素可交换。这被编码为一个类型类 Algebra R A。 从 R 到 A 的态射称为结构映射，并在 Lean 中记作 algebraMap R A : R →+* A。 对某个 r : R，将 a : A 与 algebraMap R A r 相乘被称为 a 被 r 的标量乘法，记为 r • a。 请注意，这种代数的概念有时称为 结合幺代数 (associative unital algebra)，以强调存在更一般的代数概念。

algebraMap 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

example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
    (r * r') • a = r • r' • a :=
  mul_smul r r' a

R-代数 A 和 B 之间的态射是环态射，它们与 R 元素的标量乘法可交换。它们是具有类型 AlgHom R A B 的打包态射，记号为 A →ₐ[R] B。

非交换代数的重要示例包括自同态代数和方阵代数，这两个将在线性代数一章中讨论。 在本章中，我们将讨论最重要的交换代数之一，即多项式代数。

系数在 R 中的一元多项式代数称为 Polynomial R，当打开 Polynomial 命名空间时，它可以写作 R[X]。 从 R 到 R[X] 的代数结构映射记为 C，它表示 “常数”，因为相应的多项式函数始终是常数。 未定元记为 X。

open Polynomial

example {R : Type*} [CommRing R] : R[X] := X

example {R : Type*} [CommRing R] (r : R) := X - C r

在上面的第一个示例中，至关重要的是要为 Lean 提供预期的类型，因为它无法从定义的主体中推断出来。在第二个示例中，目标多项式代数可以通过我们对 C r 的使用推断出来，因为已知 r 的类型。

由于 C 是从 R 到 R[X] 的环态射，我们可以在 R[X] 环中计算之前，使用所有环态射引理，例如 map_zero、map_one、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

可以用 Polynomial.coeff 获取系数

example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp

example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp

定义多项式的次数总是比较棘手，因为零多项式是一个特殊情况。Mathlib 有两个变体： Polynomial.natDegree : R[X] → ℕ 将零多项式的次数指定为 0，而 Polynomial.degree : R[X] → WithBot ℕ 将其指定为 ⊥。

在后者中，WithBot ℕ 可以视为 ℕ ∪ {-∞}，只不过 -∞ 被表示为 ⊥，与完备格中的底元素同一个符号。 此特殊值用于零多项式的次数，并且在加法中是吸收元。（在乘法中它几乎是吸收元，但 ⊥ * 0 = 0 除外。）

理论而言，degree 版本是正确的那一个。例如，它允许我们陈述关于乘积次数的预期公式（假设基环没有零因子）。

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    degree (p * q) = degree p + degree q :=
  Polynomial.degree_mul

而对于 natDegree 的版本，则需要假设多项式非零。

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 ℕ 更友好，因此 Mathlib 提供了这两种版本并提供了在它们之间转换的引理。此外，当计算复合多项式的次数时，natDegree 是更方便的定义。多项式的复合是 Polynomial.comp，我们有：

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    natDegree (comp p q) = natDegree p * natDegree q :=
  Polynomial.natDegree_comp

多项式产生多项式函数：任何多项式都可以通过 Polynomial.eval 在 R 上进行求值。

example {R : Type*} [CommRing R] (P: R[X]) (x : R) := P.eval x

example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp

特别地，有一个谓词 IsRoot，它用于表示当一个多项式在 R 中的某些元素 r 处取零时成立。

example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl

我们希望能够说明，在假设 R 没有零因子的情况下，一个多项式的根（按重数计算）最多不超过其次数。然而，零多项式的情况再次变得麻烦。

因此，Mathlib 定义了 Polynomial.roots，它将一个多项式 P 映射到一个多重集合（multiset），即： - 如果 P 为零多项式，该集合被定义为空集； - 否则，该集合为 P 的根，并记录其重数。

此定义仅适用于底层环是整域的情况，因为在其他情况下，该定义不具有良好的性质。

example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
  roots_X_sub_C r

example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ):
    ((X - C r) ^ n).roots = n • {r} :=
  by simp

Polynomial.eval 和 Polynomial.roots 都仅考虑系数环。它们不能让我们说明 X ^ 2 - 2 : ℚ[X] 在 ℝ 中有根，或 X ^ 2 + 1 : ℝ[X] 在 ℂ 中有根。为此，我们需要 Polynomial.aeval，它可以在任意 R-代数中对 P : R[X] 进行求值。

更具体地说，给定一个半环 A 和 Algebra R A 的实例，Polynomial.aeval 会沿着在元素 a 处的 R-代数态射将多项式的每个元素发送出去。由于 AlgHom 可以强制转换为函数，因此可以将其应用于多项式。

但 aeval 并没有一个多项式作为参数，因此不能像在上面使用 P.eval 那样使用点符号表示法。

example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp

在这种情况下，与 roots 对应的函数是 aroots，它接受一个多项式和一个代数，并输出一个多重集合（关于零多项式的警告与 roots 相同）。

open Complex Polynomial

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
    have key : (C I * C I : ℂ[X]) = -1 := by simp [← C_mul]
    rw [C_neg]
    linear_combination key
  have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
    intro H
    apply_fun eval 0 at H
    simp [eval] at H
  simp only [factored, roots_mul p_ne_zero, roots_X_sub_C]
  rfl

-- Mathlib 知晓达朗贝尔-高斯定理：``ℂ`` 是代数闭域。
example : IsAlgClosed ℂ := inferInstance

更一般地说，给定一个环态射 f : R →+* S，可以使用 Polynomial.eval₂ 在 S 中的一个点上对 P : R[X] 进行求值。 由于它不假设存在 Algebra R S 实例，因此它生成从 R[X] 到 S 的实际函数，因此点符号可以像预期那样正常工作。

#check (Complex.ofRealHom : ℝ →+* ℂ)

example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofRealHom Complex.I = 0 := by simp

我们最后简要提一下多变量多项式。给定一个交换半环 R，系数在 R 且不定元通过类型 σ 索引的多项式所构成的 R-代数为 MVPolynomial σ R。

给定 i : σ，对应的不定元记为 MvPolynomial.X i。（通常可以打开 MVPolynomial 命名空间以将其缩写为 X i。）

例如，如果我们需要两个不定元，可以使用 Fin 2 作为 σ 并写出定义单位圆的多项式（在 \(\mathbb{R}^2\) 中）如下：

open MvPolynomial

def circleEquation : MvPolynomial (Fin 2) ℝ := X 0 ^ 2 + X 1 ^ 2 - 1

函数应用具有非常高的优先级，因此上述表达式可以读取为 (X 0) ^ 2 + (X 1) ^ 2 - 1。

我们可以对其进行求值，以确保坐标为 \((1, 0)\) 的点位于圆上。 此外，![...] 表示符号表示元素属于 Fin n → X，其中自然数 n 是由参数的数量决定的，而某种类型 X 是由参数的类型决定的。

example : MvPolynomial.eval ![0, 1] circleEquation = 0 := by simp [circleEquation]