第8章层级 - 深度伴读

本章定位

本章是理解 Mathlib 架构的核心。你将学到：

extends 如何自动解决字段重叠

to_additive 自动生成加法版本

diamond problem 和 forgetful inheritance

态射的 bundled 设计和 DFunLike

SetLike 和子对象

HasQuotient 商结构

本章难度较高，建议第一遍通读理解概念，学完后续章节后再回来细读。

8.1 Basics: 构建代数层级

核心洞见

Mathlib 的代数层级从最简单的数据类开始，逐步叠加公理：One → Dia → Semigroup → Monoid → Group。

从最底层开始

class One₁ (α : Type) where
  /-- The element one -/
  one : α
 
-- class 命令做了三件事：
-- 1. 定义结构 One₁
-- 2. 标记为类型类（instance inference）
-- 3. 让 one 的 self 参数自动成为 instance-implicit
 
#check One₁.one
-- One₁.one {α : Type} [self : One₁ α] : α
--           ↑ 隐式    ↑ 实例隐式（自动推断）

对比 @[class] structure：

@[class] structure One₂ (α : Type) where
  one : α
 
#check One₂.one
-- One₂.one {α : Type} (self : One₂ α) : α
--                     ↑ 注意这里是显式参数！

class 命令的第三个效果

class 确保结构字段中的 self 参数是 instance-implicit（方括号），而 @[class] structure 不会。

自定义符号

@[inherit_doc]
notation "𝟙" => One₁.one
 
class Dia₁ (α : Type) where
  dia : α → α → α
 
infixl:70 " ⋄ " => Dia₁.dia

@[inherit_doc] 让符号 𝟙 继承 One₁.one 的文档。

extends 的核心机制

问题：如何定义 Semigroup？需要 Dia₁ 的数据 + 结合律公理。

尝试1（手动）：

class Semigroup₀ (α : Type) where
  toDia₁ : Dia₁ α
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

问题：toDia₁ 不会自动注册为 instance。

-- 失败：Lean 找不到 Dia₁ 实例
example {α : Type} [Semigroup₀ α] (a b : α) : α := a ⋄ b

需要手动添加：

attribute [instance] Semigroup₀.toDia₁

尝试2（extends，推荐）：

class Semigroup₁ (α : Type) extends toDia₁ : Dia₁ α where
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)
 
-- 成功！extends 自动注册 instance
example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b

extends 的优势

自动将父类的字段”提升”到子类

自动注册 instance

字段名可选，默认 to + 父类名

组合多个父类

class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
  one_dia : ∀ a : α, 𝟙 ⋄ a = a
  dia_one : ∀ a : α, a ⋄ 𝟙 = a
 
class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α

关键问题：字段重叠

Semigroup₁ α 和 DiaOneClass₁ α 都 extends Dia₁ α。如果手动组合，会得到两个不相关的 Dia₁ 实例！

-- 错误的方式：两个独立的 dia 操作
class Monoid₂ (α : Type) where
  toSemigroup₁ : Semigroup₁ α
  toDiaOneClass₁ : DiaOneClass₁ α
 
-- Monoid₂.toSemigroup₁.toDia₁.dia 和 Monoid₂.toDiaOneClass₁.toDia₁.dia
-- 是两个完全不同的函数！

extends 的魔法：自动解决重叠，确保只有一个 Dia₁ 实例。

example {α : Type} [Monoid₁ α] :
    (Monoid₁.toSemigroup₁.toDia₁.dia : α → α → α) = Monoid₁.toDiaOneClass₁.toDia₁.dia := rfl
-- 两者是定义上相等的！

看构造函数就明白差异：

#check Monoid₂.mk
-- Monoid₂.mk {α : Type} (toSemigroup₁ : Semigroup₁ α) (toDiaOneClass₁ : DiaOneClass₁ α) : Monoid₂ α
 
#check Monoid₁.mk
-- Monoid₁.mk {α : Type} [toSemigroup₁ : Semigroup₁ α] [toOne₁ : One₁ α]
--   (one_dia : ∀ a, 𝟙 ⋄ a = a) (dia_one : ∀ a, a ⋄ 𝟙 = a) : Monoid₁ α
--   ↑ 注意：没有单独的 DiaOneClass₁ 参数，而是拆开了！

extends 的底层行为

当两个父类共享一个祖父类时，extends 只保留一份祖父类字段，并自动生成投影保持对称性。

定义群

class Inv₁ (α : Type) where
  inv : α → α
 
@[inherit_doc]
postfix:max "⁻¹" => Inv₁.inv
 
class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
  inv_dia : ∀ a : G, a⁻¹ ⋄ a = 𝟙

只定义左逆就够了

a⁻¹ ⋄ a = 𝟙 看似太弱（只有左逆），但结合 Monoid 的公理可以推出右逆。

-- 证明思路：b = b ⋄ 𝟙 = b ⋄ (a ⋄ c) = (b ⋄ a) ⋄ c = 𝟙 ⋄ c = c
lemma left_inv_eq_right_inv₁ {M : Type} [Monoid₁ M] {a b c : M}
    (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← DiaOneClass₁.one_dia c, ← hba, Semigroup₁.dia_assoc, hac, DiaOneClass₁.dia_one b]

这个证明需要引用不同层级的定理，全名很长。用 export 简化：

export DiaOneClass₁ (one_dia dia_one)
export Semigroup₁ (dia_assoc)
export Group₁ (inv_dia)
 
-- 现在可以直接用短名
example {M : Type} [Monoid₁ M] {a b c : M}
    (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← one_dia c, ← hba, dia_assoc, hac, dia_one b]

to_additive：加法-乘法对偶

Mathlib 面临一个问题：群有加法版本（AddGroup，+）和乘法版本（Group，*），但它们的结构几乎相同。维护两套代码是浪费的。

解决方案：to_additive 属性自动从乘法版本生成加法版本。

class AddSemigroup₃ (α : Type) extends Add α where
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)
 
@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)
 
class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α
 
@[to_additive AddMonoid₃]
class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α

to_additive 的魔力

@[to_additive MyClass] 生成加法版本 MyClass

@[to_additive (attr := simp)] 同时传递 simp 属性

引理也可以自动翻译：

whatsnew in
@[to_additive]
lemma left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a b c : M}
    (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]
 
#check left_neg_eq_right_neg'  -- 自动生成的加法版本

定义环

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

Ring 的加法交换性

上面没有假设加法交换，但可以证明（利用 mul_one 和分配律）。Mathlib 中直接要求 AddCommGroup，但这里作为练习展示。

instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
  { add_comm := by sorry }

Bad Diamond Problem

定义 Module 时遇到关键问题：

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

为什么不能 extends AddCommGroup₃ M？

如果写 extends AddCommGroup₃ M，Lean 会创建实例 Module₁.toAddCommGroup₃。每当 Lean 寻找 AddCommGroup₃ M 时，它需要猜测一个完全未指定的 R 和 Ring₃ R 实例——这会导致搜索爆炸！

规则：extends 中的每个类必须提及所有类型参数。

但 SMul₃ R M 可以 extends，因为它的结果 SMul₃ R M 同时提及 R 和 M。

Bad Diamond 实例

更微妙的问题：有两个路径让 ℤ 成为 Module₁ ℤ ℤ：

        ℤ
       / \
      /   \
  Ring₃  AddCommGroup₃
      \   /
       \ /
    Module₁ ℤ ℤ

selfModule ℤ：环的自身乘法
abGrpModule ℤ：阿贝尔群的 ℤ-模结构

#synth Module₁ ℤ ℤ  -- abGrpModule ℤ

这两个路径的标量乘法定义不同，但数学上相等。Lean 可能随机选择其中一个，导致类型类推断失败。

Bad Diamond 的成因

好 diamond：底部是 Prop（如公理），任意两个证明定义上相等

坏 diamond：底部是 Type（如数据），不同构造可能不相等

解决方案：Forgetful Inheritance

在基础结构中预留数据字段，让”继承”只是”遗忘”（选择更丰富的结构中的子集），而非”重新定义”。

class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M where
  nsmul : ℕ → M → M := nsmul₁           -- 数据字段
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  nsmul_succ : ∀ n x, nsmul (n + 1) x = x + nsmul n x := by intros; rfl

对 ℤ 提供特殊实现：

instance : AddMonoid₄ ℤ where
  add := (· + ·)
  add_assoc₃ := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  nsmul := fun n m ↦ (n : ℤ) * m   -- 用整数乘法！
  nsmul_zero := Int.zero_mul
  nsmul_succ := fun n m ↦ show (n + 1 : ℤ) * m = m + n * m
    by rw [Int.add_mul, Int.add_comm, Int.one_mul]

现在两个路径的标量乘法定义上相等，diamond 问题消失。

8.2 Morphisms: 态射的设计

核心洞见

态射可以定义为谓词（predicate）或捆绑结构（bundled）。Mathlib 对代数态射用 bundled，对拓扑连续映射用 predicate。

方式1：谓词（Predicate）

def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop :=
  f 1 = 1 ∧ ∀ g g', f (g * g') = f g * f g'

缺点：用合取不方便，需要记住顺序。

方式2：结构（Structure）

structure isMonoidHom₂ [Monoid G] [Monoid H] (f : G → H) : Prop where
  map_one : f 1 = 1
  map_mul : ∀ g g', f (g * g') = f g * f g'

更好，但仍是 predicate——把函数和性质分开。

方式3：Bundled（Mathlib 的选择）

@[ext]
structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H] where
  toFun : G → H
  map_one : toFun 1 = 1
  map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

为什么选择 bundled？

代数态射是”名词”而非”形容词”。你很少遇到不是群同态的群之间函数。 bundled 更方便组织成层级。

Coercion：像函数一样使用

instance [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := MonoidHom₁.toFun
 
attribute [coe] MonoidHom₁.toFun
 
-- 现在可以像函数一样使用 MonoidHom
example [Monoid G] [Monoid H] (f : MonoidHom₁ G H) : f 1 = 1 := f.map_one

attribute [coe] 让 Lean 在显示时用 ↑ 前缀，保持 tactic state 整洁。

态射的层级

@[ext]
structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H] where
  toFun : G → H
  map_zero : toFun 0 = 0
  map_add : ∀ g g', toFun (g + g') = toFun g + toFun g'
 
@[ext]
structure RingHom₁ (R S : Type) [Ring R] [Ring S]
    extends MonoidHom₁ R S, AddMonoidHom₁ R S

问题：MonoidHom 的引理不能直接用于 RingHom

RingHom₁.toMonoidHom₁ 需要显式转换。

解决方案：MonoidHomClass

class MonoidHomClass₂ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

outParam 的作用

outParam 告诉 Lean：先确定 F，再推断 M 和 N。没有它，Lean 面对 f x 时会先猜 M 和 N，导致搜索爆炸。

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N where
  toFun := MonoidHom₁.toFun
  map_one := fun f ↦ f.map_one
  map_mul := fun f ↦ f.map_mul
 
instance (R S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S where
  toFun := fun f ↦ f.toMonoidHom₁.toFun
  map_one := fun f ↦ f.toMonoidHom₁.map_one
  map_mul := fun f ↦ f.toMonoidHom₁.map_mul

现在可以写通用引理：

lemma map_inv_of_inv [Monoid M] [Monoid N] [MonoidHomClass₂ F M N]
    (f : F) {m m' : M} (h : m * m' = 1) : f m * f m' = 1 := by
  rw [← MonoidHomClass₂.map_mul, h, MonoidHomClass₂.map_one]
 
-- 同时适用于 MonoidHom 和 RingHom！
example [Monoid M] [Monoid N] (f : MonoidHom₁ M N) {m m' : M} (h : m * m' = 1) :
    f m * f m' = 1 := map_inv_of_inv f h
 
example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r * r' = 1) :
    f r * f r' = 1 := map_inv_of_inv f h

DFunLike：进一步抽象

MonoidHomClass₂ 中仍有重复的 toFun 和 CoeFun 代码。Mathlib 用 DFunLike（Dependent Function Like）统一：

class MonoidHomClass₃ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N]
    extends DFunLike F M (fun _ ↦ N) where
  map_one : ∀ f : F, f 1 = 1
  map_mul : ∀ (f : F) g g', f (g * g') = f g * f g'
 
instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₃ (MonoidHom₁ M N) M N where
  coe := MonoidHom₁.toFun
  coe_injective' _ _ := MonoidHom₁.ext
  map_one := MonoidHom₁.map_one
  map_mul := MonoidHom₁.map_mul

DFunLike 同时处理 coercion 到函数和注入性证明，减少重复代码。

8.3 Sub-objects: 子对象

核心洞见

子对象 = 子集 + 封闭性。用 SetLike 统一处理。

Submonoid

@[ext]
structure Submonoid₁ (M : Type) [Monoid M] where
  carrier : Set M
  mul_mem {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
  one_mem : 1 ∈ carrier

SetLike：统一子对象接口

instance [Monoid M] : SetLike (Submonoid₁ M) M where
  coe := Submonoid₁.carrier
  coe_injective' _ _ := Submonoid₁.ext

SetLike 提供：

Coercion to Set：N : Submonoid₁ M 可当作 Set M 用
Membership：1 ∈ N 而不是 1 ∈ N.carrier
Coercion to Type：(x : N) 表示”N 中的元素”

example [Monoid M] (N : Submonoid₁ M) : 1 ∈ N := N.one_mem
 
example [Monoid M] (N : Submonoid₁ M) (α : Type) (f : M → α) := f '' N
 
-- x : N 可强制转换为 M
example [Monoid M] (N : Submonoid₁ M) (x : N) : (x : M) ∈ N := x.property

子对象继承代数结构

instance SubMonoid₁Monoid [Monoid M] (N : Submonoid₁ M) : Monoid N where
  mul := fun x y ↦ ⟨x * y, N.mul_mem x.property y.property⟩
  mul_assoc := fun x y z ↦ SetCoe.ext (mul_assoc (x : M) y z)
  one := ⟨1, N.one_mem⟩
  one_mul := fun x ↦ SetCoe.ext (one_mul (x : M))
  mul_one := fun x ↦ SetCoe.ext (mul_one (x : M))

SetCoe.ext 的作用

SetCoe.ext 证明 coercion 是单射：如果 (x : M) = (y : M)，那么 x = y。

子对象构成格

Mathlib 中，任何代数对象的子对象都形成完备格（complete lattice）：

instance [Monoid M] : Min (Submonoid₁ M) :=
  ⟨fun S₁ S₂ ↦
    { carrier := S₁ ∩ S₂
      one_mem := ⟨S₁.one_mem, S₂.one_mem⟩
      mul_mem := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ ↦ ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

为什么用 ⊓ 而不是 ∩？

子对象的并集不一定是子对象（例如两个子群的并集一般不是子群）。用 ⊓（infimum）和 ⊔（supremum）表示格运算更统一：

N ⊓ P = 最大的同时包含于 N 和 P 的子对象 = 交集

N ⊔ P = 最小的同时包含 N 和 P 的子对象 = 生成的子对象

Quotient：商结构

HasQuotient 类提供 M ⧸ N 符号：

-- 注意：⧸ 是特殊 unicode，不是 /
instance [CommMonoid M] : HasQuotient M (Submonoid M) where
  quotient' := fun N ↦ Quotient N.Setoid

构造商单形需要定义等价关系、证明它是等价关系，然后在商上定义运算：

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M where
  r := fun x y ↦ ∃ w ∈ N, ∃ z ∈ N, x * w = y * z
  iseqv := {
    refl := fun x ↦ ⟨1, N.one_mem, 1, N.one_mem, rfl⟩
    symm := fun ⟨w, hw, z, hz, h⟩ ↦ ⟨z, hz, w, hw, h.symm⟩
    trans := by sorry
  }

本章核心概念总结

概念	用途	关键细节
`extends`	继承并自动解决重叠	只保留一份共享字段
`to_additive`	自动生成加法版本	乘法引理 → 加法引理
Bad Diamond	多个路径到同一结构	数据字段定义不同时出错
Forgetful Inheritance	解决 bad diamond	预留字段，特殊实例覆盖
`outParam`	控制类型推断顺序	先推断 morphism 类型
`DFunLike`	统一 bundled 函数	处理 coercion 和注入性
`SetLike`	统一子对象	coercion 到 Set 和 Type
`HasQuotient`	商结构符号	`M ⧸ N`

关键设计原则

1. 何时用 bundled vs predicate？

情况	选择	例子

大多数函数都是态射 | Bundled | MonoidHom, RingHom | | 只有部分函数满足 | Predicate | Continuous, Monotone |

2. extends 的规则

extends 中的每个类必须提及所有类型参数

3. 避免 bad diamond

让"继承" = "遗忘数据"，而不是"重新定义数据"

预告：第9章会学到什么

第9章应用层级概念：

群和幺半群的性质
环、域的性质
group, field_simp 等专用 tactic

自测问题

extends 和手动组合父类有什么区别？为什么字段重叠是个问题？

to_additive 解决什么问题？它是如何工作的？

什么是 bad diamond？如何用 forgetful inheritance 解决？

为什么 MonoidHomClass 需要 outParam？

SetLike 提供了哪些便利？

子对象的 ⊔ 和集合的 ∪ 有什么区别？

伴读文档 - 第8章完

我的博客

探索

Ch8 层级 - 深度伴读

第8章层级 - 深度伴读

8.1 Basics: 构建代数层级

从最底层开始

自定义符号

extends 的核心机制

组合多个父类

定义群

to_additive：加法-乘法对偶

定义环

Bad Diamond Problem

Bad Diamond 实例

8.2 Morphisms: 态射的设计

方式1：谓词（Predicate）

方式2：结构（Structure）

方式3：Bundled（Mathlib 的选择）

Coercion：像函数一样使用

态射的层级

解决方案：MonoidHomClass

DFunLike：进一步抽象

8.3 Sub-objects: 子对象

Submonoid

SetLike：统一子对象接口

子对象继承代数结构

子对象构成格

Quotient：商结构

本章核心概念总结

关键设计原则

1. 何时用 bundled vs predicate？

2. extends 的规则

3. 避免 bad diamond

预告：第9章会学到什么

关系图谱

目录

反向链接

我的博客

探索

Ch8 层级 - 深度伴读

第8章 层级 - 深度伴读

8.1 Basics: 构建代数层级

从最底层开始

自定义符号

extends 的核心机制

组合多个父类

定义群

to_additive：加法-乘法对偶

定义环

Bad Diamond Problem

Bad Diamond 实例

8.2 Morphisms: 态射的设计

方式1：谓词（Predicate）

方式2：结构（Structure）

方式3：Bundled（Mathlib 的选择）

Coercion：像函数一样使用

态射的层级

解决方案：MonoidHomClass

DFunLike：进一步抽象

8.3 Sub-objects: 子对象

Submonoid

SetLike：统一子对象接口

子对象继承代数结构

子对象构成格

Quotient：商结构

本章核心概念总结

关键设计原则

1. 何时用 bundled vs predicate？

2. extends 的规则

3. 避免 bad diamond

预告：第9章会学到什么

关系图谱

目录

反向链接

第8章层级 - 深度伴读