7. 层次结构

在 第 6 章 中，我们已经了解了如何定义群类并创建此类的实例，以及如何创建交换环类的实例。但当然这里存在一个层次结构：交换环尤其是一种加法群。在本章中，我们将研究如何构建这样的层次结构。它们出现在数学的所有分支中，但在本章中，重点将放在代数示例上。 在更多地讨论如何使用现有的层级结构之前，就来探讨如何构建层级结构似乎为时尚早。但要使用层级结构，就需要对其底层技术有一定的了解。所以您或许还是应该读一下这一章，不过在第一次阅读时不必太努力记住所有内容，先读完后面的章节，然后再回过头来重读这一章。 在这一章中，我们将重新定义（更简单的版本）出现在 Mathlib 中的许多内容，因此我们将使用索引来区分我们的版本。例如，我们将把我们的版本的 Ring 称为 Ring₁ 。由于我们将逐步介绍更强大的形式化结构的方法，这些索引有时会超过 1。

7.1. 基础

在Lean的所有层次结构的最底层，我们能找到承载数据的类。下面这个类记录了给定类型 α 具有一个被称为 one 的特殊元素。在现阶段，它没有任何属性。

class One₁ (α : Type) where
  /-- The element one -/
  one : α

由于在本章中我们将更频繁地使用类，所以我们需要进一步了解 class 命令的作用。 首先，上述的 class 命令定义了一个结构体 One₁ ，其参数为 α : Type ，且只有一个字段 one 。它还标记此结构体为类，这样对于某些类型 α 的 One₁ α 类型的参数，只要它们被标记为实例隐式参数（即出现在方括号中），就可以通过实例解析过程进行推断。 这两个效果也可以通过带有 class 属性的 structure 命令来实现，即写成 @[class] structure 的形式。但 class 命令还确保了 One₁ α 在其自身的字段中以实例隐式参数的形式出现。比较：

#check One₁.one -- One₁.one {α : Type} [self : One₁ α] : α

@[class] structure One₂ (α : Type) where
  /-- The element one -/
  one : α

#check One₂.one

在第二次检查中，我们可以看到 self : One₂ α 是一个显式参数。 让我们确保第一个版本确实可以在没有任何显式参数的情况下使用。

example (α : Type) [One₁ α] : α := One₁.one

备注：在上述示例中，参数 One₁ α 被标记为实例隐式，这有点蠢，因为这仅影响该声明的 使用 ，而由 example 命令创建的声明无法被使用。不过，这使我们能够避免为该参数命名，更重要的是，它开始养成将 One₁ α 参数标记为实例隐式的良好习惯。

另一个需要注意的地方是，只有当 Lean 知道 α 是什么时，上述所有内容才会起作用。在上述示例中，如果省略类型标注 : α ，则会生成类似以下的错误消息：

typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α)

其中 ?m.263 α 表示“依赖于 α 的某种类型”（263 只是一个自动生成的索引，用于区分多个未知事物）。另一种避免此问题的方法是使用类型注解，例如：

example (α : Type) [One₁ α] := (One₁.one : α)

如果您在 Section 3.6 中尝试处理数列的极限时遇到过这个问题，那么您可能已经遇到过这种情况，比如您试图声明 0 < 1 ，但没有告诉 Lean 您是想表示自然数之间的不等式还是实数之间的不等式。

我们的下一个任务是为 One₁.one 指定一个符号。由于我们不想与内置的 1 符号发生冲突，我们将使用 𝟙 。这是通过以下命令实现的，其中第一行告诉 Lean 使用 One₁.one 的文档作为符号 𝟙 的文档。

@[inherit_doc]
notation "𝟙" => One₁.one

example {α : Type} [One₁ α] : α := 𝟙

example {α : Type} [One₁ α] : (𝟙 : α) = 𝟙 := rfl

我们现在想要一个记录二元运算的数据承载类。目前我们不想在加法和乘法之间做出选择，所以我们将使用菱形。

class Dia₁ (α : Type) where
  dia : α → α → α

infixl:70 " ⋄ "   => Dia₁.dia

与 One₁ 示例一样，此时该运算没有任何属性。现在让我们定义一个半群结构类，其中运算用 ⋄ 表示。目前，我们手动将其定义为具有两个字段的结构，一个 Dia₁ 实例和一个值为 Prop 的字段 dia_assoc ，用于断言 ⋄ 的结合性。

class Semigroup₁ (α : Type) where
  toDia₁ : Dia₁ α
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

请注意，在声明 dia_assoc 时，先前定义的字段 toDia₁ 在本地上下文中，因此在 Lean 搜索 Dia₁ α 的实例以理解 a ⋄ b 时可以使用它。但是这个 toDia₁ 字段不会成为类型类实例数据库的一部分。因此，执行 example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b 将会失败。错误消息 failed to synthesize instance Dia₁ α 。

我们可以通过稍后添加 instance 属性来解决这个问题。

attribute [instance] Semigroup₁.toDia₁

example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b

在构建之前，我们需要一种比显式编写诸如 toDia₁ 这样的字段并手动添加实例属性更方便的方式来扩展结构。 class 使用如下语法通过 extends 支持这一点：

class Semigroup₂ (α : Type) extends Dia₁ α where
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

example {α : Type} [Semigroup₂ α] (a b : α) : α := a ⋄ b

请注意，这种语法在 structure 命令中也是可用的，尽管在这种情况下，它仅解决了编写诸如 toDia₁ 这样的字段的麻烦，因为在那种情况下没有实例需要定义。

现在让我们尝试将一个菱形运算和一个特殊操作结合起来，并用公理说明这个元素在两边都是零元。

class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
  /-- 存在一个对于菱形运算的左零元。 -/
  one_dia : ∀ a : α, 𝟙 ⋄ a = a
  /-- 存在一个对于菱形运算的右零元。 -/
  dia_one : ∀ a : α, a ⋄ 𝟙 = a

在下一个示例中，我们告诉 Lean α 具有 DiaOneClass₁ 结构，并声明一个使用 Dia₁ 实例和 One₁ 实例的属性。为了查看 Lean 如何找到这些实例，我们设置了一个跟踪选项，其结果可以在 Infoview 中看到。默认情况下，该结果相当简略，但可以通过点击以黑色箭头结尾的行来展开。它包括 Lean 在拥有足够的类型信息之前尝试查找实例但未成功的尝试。成功的尝试确实涉及由 extends 语法生成的实例。

set_option trace.Meta.synthInstance true in
example {α : Type} [DiaOneClass₁ α] (a b : α) : Prop := a ⋄ b = 𝟙

请注意，在组合现有类时，我们不需要包含额外的字段。因此，我们可以将半群定义为：

class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α

虽然上述定义看起来很简单，但它隐藏了一个重要的微妙之处。 Semigroup₁ α 和 DiaOneClass₁ α 都扩展了 Dia₁ α ，所以有人可能会担心，拥有一个 Monoid₁ α 实例会在 α 上产生两个不相关的菱形运算，一个来自字段 Monoid₁.toSemigroup₁ ，另一个来自字段 Monoid₁.toDiaOneClass₁ 。

实际上，如果我们尝试通过以下方式手动构建一个单子类：

class Monoid₂ (α : Type) where
  toSemigroup₁ : Semigroup₁ α
  toDiaOneClass₁ : DiaOneClass₁ α

那么我们会得到两个完全不相关的菱形运算

Monoid₂.toSemigroup₁.toDia₁.dia 和 Monoid₂.toDiaOneClass₁.toDia₁.dia 。

使用 extends 语法生成的版本不存在此缺陷。

example {α : Type} [Monoid₁ α] :
  (Monoid₁.toSemigroup₁.toDia₁.dia : α → α → α) = Monoid₁.toDiaOneClass₁.toDia₁.dia := rfl

所以 class 命令为我们做了些神奇的事（ structure 命令也会这样做）。查看类的构造函数是了解其字段的简便方法。比较：

/- 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₁ α -/
#check Monoid₁.mk

所以我们看到 Monoid₁ 按预期接受 Semigroup₁ α 参数，但不会接受可能重叠的 DiaOneClass₁ α 参数，而是将其拆分并仅包含不重叠的部分。它还自动生成了一个实例 Monoid₁.toDiaOneClass₁ ，这并非字段，但具有预期的签名，从最终用户的角度来看，这恢复了两个扩展类 Semigroup₁ 和 DiaOneClass₁ 之间的对称性。

#check Monoid₁.toSemigroup₁
#check Monoid₁.toDiaOneClass₁

我们现在离定义群非常接近了。我们可以在单子结构中添加一个字段，断言每个元素都存在逆元。但那样的话，我们需要努力才能访问这些逆元。实际上，将其作为数据添加会更方便。为了优化可重用性，我们定义一个新的携带数据的类，然后为其提供一些符号表示。

class Inv₁ (α : Type) where
  /-- The inversion function -/
  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 的左逆元。但另一侧是自动的。为了证明这一点，我们需要一个预备引理。

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]

现在轮到你来证明我们代数结构的性质了。

lemma inv_eq_of_dia [Group₁ G] {a b : G} (h : a ⋄ b = 𝟙) : a⁻¹ = b :=
  sorry

lemma dia_inv [Group₁ G] (a : G) : a ⋄ a⁻¹ = 𝟙 :=
  sorry

在这个阶段，我们想继续定义环，但有一个严重的问题。一个类型的环结构包含一个加法群结构和一个乘法半群结构，以及它们相互作用的一些性质。但到目前为止，我们为所有操作硬编码了一个符号 ⋄ 。更根本的是，类型类系统假定每个类型对于每个类型类只有一个实例。有多种方法可以解决这个问题。令人惊讶的是，Mathlib 使用了一个朴素的想法，借助一些代码生成属性，为加法和乘法理论复制了所有内容。结构和类以加法和乘法两种记法定义，并通过属性 to_additive 相互关联。对于像半群这样的多重继承情况，自动生成的“恢复对称性”的实例也需要进行标记。这有点技术性，您无需理解细节。重要的是，引理仅以乘法记法陈述，并通过属性 to_additive 标记，以生成加法版本为 left_inv_eq_right_inv' ，其自动生成的加法版本为 left_neg_eq_right_neg' 。为了检查这个加法版本的名称，我们在 left_inv_eq_right_inv' 之上使用了 whatsnew in 命令。

class AddSemigroup₃ (α : Type) extends Add α where
/-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
/-- Multiplication is associative -/
  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 α

attribute [to_additive existing] Monoid₃.toMulOneClass

export Semigroup₃ (mul_assoc₃)
export AddSemigroup₃ (add_assoc₃)

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 AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
  add_comm : ∀ a b : α, a + b = b + a

@[to_additive AddCommSemigroup₃]
class CommSemigroup₃ (α : Type) extends Semigroup₃ α where
  mul_comm : ∀ a b : α, a * b = b * a

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

@[to_additive AddCommMonoid₃]
class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α

class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
  neg_add : ∀ a : G, -a + a = 0

@[to_additive AddGroup₃]
class Group₃ (G : Type) extends Monoid₃ G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1

我们应当在适当的时候用 simp 标记引理。

attribute [simp] Group₃.inv_mul AddGroup₃.neg_add

然后我们需要重复一些工作，因为我们切换到标准记法，但至少 to_additive 完成了从乘法记法到加法记法的转换工作。

@[to_additive]
lemma inv_eq_of_mul [Group₃ G] {a b : G} (h : a * b = 1) : a⁻¹ = b :=
  sorry

请注意，可以要求 to_additive 为一个引理添加 simp 标签，并将该属性传播到加法版本，如下所示。

@[to_additive (attr := simp)]
lemma Group₃.mul_inv {G : Type} [Group₃ G] {a : G} : a * a⁻¹ = 1 := by
  sorry

@[to_additive]
lemma mul_left_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : a * b = a * c) : b = c := by
  sorry

@[to_additive]
lemma mul_right_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : b*a = c*a) : b = c := by
  sorry

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

@[to_additive AddCommGroup₃]
class CommGroup₃ (G : Type) extends Group₃ G, CommMonoid₃ G

现在我们准备讨论环。为了演示目的，我们不会假设加法是交换的，然后立即提供一个 AddCommGroup₃ 的实例。Mathlib 不会玩这种把戏，首先是因为在实践中这不会使任何环实例变得更容易，其次是因为 Mathlib 的代数层次结构通过半环进行，半环类似于环但没有相反数，因此下面的证明对它们不起作用。在这里，我们不仅收获了一个不错的实践机会（尤其是对于初次接触者而言），更能通过这一过程掌握一个实例构建的范例，其中运用了能够同时指定父结构及额外字段的语法技巧。

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
  /-- Multiplication is left distributive over addition -/
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  /-- Multiplication is right distributive over addition -/
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

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

当然，我们也可以构建具体的实例，比如在整数上构建环结构（当然下面的实例利用了 Mathlib 中已经完成的所有工作）。

instance : Ring₃ ℤ where
  add := (· + ·)
  add_assoc₃ := add_assoc
  zero := 0
  zero_add := by simp
  add_zero := by simp
  neg := (- ·)
  neg_add := by simp
  mul := (· * ·)
  mul_assoc₃ := mul_assoc
  one := 1
  one_mul := by simp
  mul_one := by simp
  zero_mul := by simp
  mul_zero := by simp
  left_distrib := Int.mul_add
  right_distrib := Int.add_mul

作为练习，您现在可以为序关系设置一个简单的层次结构，包括一个有序交换幺半群的类，它同时具有偏序关系和交换幺半群结构，满足 ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b 。当然，您需要为以下类添加字段，可能还需要添加 extends 子句。

class LE₁ (α : Type) where
  /-- The Less-or-Equal relation. -/
  le : α → α → Prop

@[inherit_doc] infix:50 " ≤₁ " => LE₁.le

class Preorder₁ (α : Type)

class PartialOrder₁ (α : Type)

class OrderedCommMonoid₁ (α : Type)

instance : OrderedCommMonoid₁ ℕ where

我们现在要讨论涉及多个类型的代数结构。最典型的例子是环上的模。如果您不知道什么是模，您可以假装它指的是向量空间，并认为我们所有的环都是域。这些结构是配备了某个环的元素的标量乘法的交换加法群。

我们首先定义由某种类型 α 在某种类型 β 上进行标量乘法的数据承载类型类，并为其赋予右结合的表示法。

class SMul₃ (α : Type) (β : Type) where
  /-- Scalar multiplication -/
  smul : α → β → β

infixr:73 " • " => SMul₃.smul

然后我们可以定义模（如果您不知道什么是模，可以先想想向量空间）。

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

这里有一些有趣的事情。虽然 R 上的环结构作为此定义的参数并不令人意外，但您可能期望 AddCommGroup₃ M 像 SMul₃ R M 一样成为 extends 子句的一部分。尝试这样做会导致一个听起来很神秘的错误消息： cannot find synthesization order for instance Module₁.toAddCommGroup₃ with type (R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M all remaining arguments have metavariables: Ring₃ ?R @Module₁ ?R ?inst✝ M。 要理解此消息，您需要记住，这样的 extends 子句会导致一个标记为实例的字段 Module₃.toAddCommGroup₃ 。此实例具有错误消息中出现的签名：

(R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M 。在类型类数据库中有这样一个实例，每次 Lean 要为某个 M 查找一个 AddCommGroup₃ M 实例时，它都需要先去寻找一个完全未指定的类型 R 以及一个 Ring₃ R 实例，然后才能开始寻找主要目标，即一个 Module₁ R M 实例。这两个支线任务在错误消息中由元变量表示，并在那里用 ？R 和 ？inst✝ 标注。这样的一个 Module₃.toAddCommGroup₃ 实例对于实例解析过程来说会是一个巨大的陷阱，因此 class 命令拒绝设置它。

那么 extends SMul₃ R M 又如何呢？它创建了一个字段

Module₁.toSMul₃ : {R : Type} →  [inst : Ring₃ R] → {M : Type} → [inst_1 : AddCommGroup₃ M] → [self : Module₁ R M] → SMul₃ R M

其最终结果 SMul₃ R M 同时提到了 R 和 M ，所以这个字段可以安全地用作实例。规则很容易记住：在 extends 子句中出现的每个类都应提及参数中出现的每个类型。

让我们创建我们的第一个模块实例：一个环自身就是一个模块，其乘法作为标量乘法。

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
  smul := fun r s ↦ r*s
  zero_smul := zero_mul
  one_smul := one_mul
  mul_smul := mul_assoc₃
  add_smul := Ring₃.right_distrib
  smul_add := Ring₃.left_distrib

作为第二个例子，每个阿贝尔群都是整数环上的模块（这是推广向量空间理论以允许非可逆标量的原因之一）。首先，对于任何配备零和加法的类型，都可以定义自然数的标量乘法： n • a 定义为 a + ⋯ + a ，其中 a 出现 n 次。然后通过确保 (-1) • a = -a 将其扩展到整数的标量乘法。

def nsmul₁ [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | n + 1, a => a + nsmul₁ n a

def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M
  | Int.ofNat n, a => nsmul₁ n a
  | Int.negSucc n, a => -nsmul₁ n.succ a

证明这会产生一个模块结构有点繁琐，且对当前讨论来说不那么有趣，所以我们很抱歉地略过所有公理。您**无需**用证明来替换这些抱歉。如果您坚持这样做，那么您可能需要陈述并证明关于 nsmul₁ 和 zsmul₁ 的几个中间引理。

instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
  smul := zsmul₁
  zero_smul := sorry
  one_smul := sorry
  mul_smul := sorry
  add_smul := sorry
  smul_add := sorry

一个更为重要的问题是，我们目前对于整数环 ℤ 本身存在两种模块结构：首先，由于 ℤ 是阿贝尔群，因此可以定义其为 abGrpModule ℤ ；其次，鉴于 ℤ 作为环的性质，我们也可以将其视作 selfModule ℤ 。这两种模块结构虽然对应相同的阿贝尔群结构，但它们在标量乘法上的一致性并不显而易见。实际上，这两者确实是相同的，但这一点并非由定义直接决定，而需要通过证明来确认。这一情况对类型类实例解析过程而言无疑是个不利消息，并且可能会让使用此层次结构的用户感到颇为沮丧。当我们直接请求找到某个实例时，Lean 会自动选择一个，我们可以通过以下命令查看所选的是哪一个：

#synth Module₁ ℤ ℤ -- abGrpModule ℤ

但在更间接的上下文中，Lean 可能会先推断出一个实例，然后感到困惑。这种情况被称为坏菱形。这与我们上面使用的菱形运算无关，而是指从 ℤ 到其 Module₁ ℤ 的路径，可以通过 AddCommGroup₃ ℤ 或 Ring₃ ℤ 中的任意一个到达。

重要的是要明白，并非所有的菱形结构都是不好的。实际上，在 Mathlib 中以及本章中到处都有菱形结构。在最开始的时候我们就看到，可以从 Monoid₁ α 通过 Semigroup₁ α 或者 DiaOneClass₁ α 到达 Dia₁ α ，并且由于 class 命令所做的工作，这两个 Dia₁ α 实例在定义上是相等的。特别是，底部为 Prop 值类的菱形结构不可能是不好的，因为对同一陈述的任何两个证明在定义上都是相等的。

但是我们用模块创建的菱形肯定是有问题的。问题出在 smul 字段上，它是数据而非证明，并且我们有两个构造在定义上并不相等。解决这个问题的稳健方法是确保从丰富结构到贫乏结构的转换总是通过遗忘数据来实现，而不是通过定义数据。这种众所周知的模式被称为“遗忘继承”，在 https://inria.hal.science/hal-02463336 中有大量讨论。

在我们的具体案例中，我们可以修改 AddMonoid₃ 的定义，以包含一个 nsmul 数据字段以及一些值为 Prop 类型的字段，以确保此操作确实是我们在上面构造的那个。在下面的定义中，这些字段在其类型后面使用 := 给出了默认值。由于这些默认值的存在，大多数实例的构造方式与我们之前的定义完全相同。但在 ℤ 的特殊情况下，我们将能够提供特定的值。

class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M where
  /-- Multiplication by a natural number. -/
  nsmul : ℕ → M → M := nsmul₁
  /-- Multiplication by `(0 : ℕ)` gives `0`. -/
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
  nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl

instance mySMul {M : Type} [AddMonoid₄ M] : SMul ℕ M := ⟨AddMonoid₄.nsmul⟩

让我们检查一下，即使不提供与 nsmul 相关的字段，我们是否仍能构造一个乘积单群实例。

instance (M N : Type) [AddMonoid₄ M] [AddMonoid₄ N] : AddMonoid₄ (M × N) where
  add := fun p q ↦ (p.1 + q.1, p.2 + q.2)
  add_assoc₃ := fun a b c ↦ by ext <;> apply add_assoc₃
  zero := (0, 0)
  zero_add := fun a ↦ by ext <;> apply zero_add
  add_zero := fun a ↦ by ext <;> apply add_zero

现在让我们处理 ℤ 的特殊情况，在这种情况下，我们希望使用从 ℕ 到 ℤ 的强制转换以及 ℤ 上的乘法来构建 nsmul 。请注意，特别是证明字段包含的工作比上面的默认值要多。

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]

让我们检查一下我们是否解决了问题。因为 Lean 已经有一个自然数和整数的标量乘法定义，而我们希望确保使用我们的实例，所以我们不会使用 • 符号，而是调用 SMul.mul 并明确提供上面定义的实例。

example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl

接下来的故事中，会在群的定义中加入一个 zsmul 字段，并采用类似的技巧。现在您已经准备好阅读 Mathlib 中关于幺半群、群、环和模的定义了。它们比我们在这里看到的要复杂，因为它们属于一个庞大的层级结构，但上面已经解释了所有原则。

作为练习，您可以回到上面构建的序关系层次结构，并尝试引入一个携带“小于”符号 <₁ 的类型类 LT₁，并确保每个预序都带有一个 <₁，其默认值由 ≤₁ 构建，并且有一个 Prop 值字段，断言这两个比较运算符之间的自然关系。 -/

7.2. 态射

到目前为止，在本章我们讨论了如何创建数学结构的层次结构。 但定义结构的工作尚未完成，除非我们有了态射。这里主要有两种方法。最显而易见的方法是在函数上定义一个谓词。

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

在这个定义中，使用合取有点不自然。特别是用户在想要访问这两个条件时，需要记住我们选择的顺序。所以我们可以使用一个结构来替代。

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'

一旦到了这里，不禁让人考虑将其设计为一个类，并使用类型类实例解析过程自动推断复杂函数的 isMonoidHom₂ ，基于简单函数的实例。例如，两个幺半群态射的复合也是一个幺半群态射，这似乎是一个有用的实例。然而，这样的实例对于解析过程来说会非常棘手，因为它需要在每个地方寻找 g ∘ f 。在 g (f x) 中找不到它会非常令人沮丧。更一般地说，必须始终牢记，识别给定表达式中应用了哪个函数是一个非常困难的问题，称为“高阶合一问题”。因此，Mathlib 并不采用这种类的方法。

一个更根本的问题在于，我们是像上面那样使用谓词（无论是使用 def 还是 structure ），还是使用将函数和谓词捆绑在一起的结构。这在一定程度上是一个心理问题。考虑两个幺半群之间的函数，而该函数不是同态的情况极为罕见。感觉“幺半群同态”不是一个可以赋予裸函数的形容词，而是一个名词。另一方面，有人可能会说，拓扑空间之间的连续函数实际上是一个恰好连续的函数。这就是为什么 Mathlib 有一个 Continuous 谓词的原因。例如，您可以这样写：

example : Continuous (id : ℝ → ℝ) := continuous_id

我们仍然有连续函数的束，这在例如为连续函数空间赋予拓扑时很方便，但它们不是处理连续性的主要工具。

相比之下，单子（或其他代数结构）之间的态射是捆绑在一起的，例如：

@[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'

当然，我们不想到处都输入 toFun ，所以我们使用 CoeFun 类型类来注册一个强制转换。它的第一个参数是我们想要强制转换为函数的类型。第二个参数描述目标函数类型。在我们的例子中，对于每个 f : MonoidHom₁ G H ，它总是 G → H 。我们还用 coe 属性标记 MonoidHom₁.toFun ，以确保它在策略状态中几乎不可见，仅通过 ↑ 前缀显示。

instance [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := MonoidHom₁.toFun

attribute [coe] MonoidHom₁.toFun

让我们检查一下我们是否确实可以将捆绑的单子态射应用于一个元素。

example [Monoid G] [Monoid H] (f : MonoidHom₁ G H) : f 1 = 1 :=  f.map_one

于其他类型的态射，我们也可以做同样的事情，直到我们遇到环态射。

@[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'

instance [AddMonoid G] [AddMonoid H] : CoeFun (AddMonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := AddMonoidHom₁.toFun

attribute [coe] AddMonoidHom₁.toFun

@[ext]
structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S

这种方法存在一些问题。一个小问题是，我们不太清楚在哪里放置 coe 属性，因为 RingHom₁.toFun 并不存在，相关函数是 MonoidHom₁.toFun ∘ RingHom₁.toMonoidHom₁ ，这并不是一个可以标记属性的声明（但我们仍然可以定义一个 CoeFun  (RingHom₁ R S) (fun _ ↦ R → S) 实例）。一个更重要的问题是，关于单子态射的引理不能直接应用。这将归结为要么每次应用单群同态引理时都与 RingHom₁.toMonoidHom₁ 打交道，要么为环同态重新陈述每个这样的引理。这两种选择都不吸引人，因此 Mathlib 在这里使用了一个新的层次结构技巧。其想法是定义一个至少为单群同态的对象的类型类，用单群同态和环同态实例化该类，并使用它来陈述每个引理。在下面的定义中， F 可以是 MonoidHom₁ M N ，或者如果 M 和 N 具有环结构，则为 RingHom₁ M N 。

class MonoidHomClass₁ (F : Type) (M N : 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'

然而，上述实现存在一个问题。我们尚未注册到函数实例的强制转换。让我们现在尝试这样做。

def badInst [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₁.toFun

将此设为实例是不好的。当面对类似 f x 的情况，而 f 的类型不是函数类型时，Lean 会尝试查找一个 CoeFun 实例来将 f 转换为函数。上述函数的类型为：

{M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N)

因此，在尝试应用它时，Lean 无法预先确定未知类型 M 、 N 和 F 应该以何种顺序进行推断。这与我们之前看到的情况略有不同，但归根结底是同一个问题：在不知道 M 的情况下，Lean 将不得不在未知类型上搜索单子实例，从而无望地尝试数据库中的每一个单子实例。如果您想看看这种实例的效果，可以在上述声明的顶部输入 set_option synthInstance.checkSynthOrder false in ，将 def badInst 替换为 instance ，然后在这个文件中查找随机出现的错误。

在这里，解决方案很简单，我们需要告诉 Lean 先查找什么是 F ，然后再推导出 M 和 N 。这可以通过使用 outParam 函数来实现。该函数被定义为恒等函数，但仍会被类型类机制识别，并触发所需的行为。因此，我们可以重新定义我们的类，注意使用 outParam 函数：

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'

instance [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₂.toFun

attribute [coe] MonoidHomClass₂.toFun

现在我们可以继续执行我们的计划，实例化这个类了。

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

正如所承诺的那样，我们对 f : F 在假设存在 MonoidHomClass₁ F 的实例的情况下所证明的每个引理，都将同时适用于幺半群同态和环同态。让我们来看一个示例引理，并检查它是否适用于这两种情况。

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]

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

乍一看，可能会觉得我们又回到了之前那个糟糕的想法，即把 MonoidHom₁ 设为一个类。 但其实并非如此。一切都提升了一个抽象层次。类型类解析过程不会寻找函数，而是寻找 MonoidHom₁ 或者 RingHom₁ 。

我们方法中仍存在的一个问题是在围绕 toFun 字段以及相应的 CoeFun 实例和 coe 属性的地方存在重复代码。另外，最好记录下这种模式仅用于具有额外属性的函数，这意味着对函数的强制转换应该是单射的。因此，Mathlib 在这个基础层之上又增加了一层抽象，即基础类 DFunLike （其中“DFun”代表依赖函数）。让我们基于这个基础层重新定义我们的 MonoidHomClass 。

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

当然，态射的层次结构不止于此。我们还可以继续定义一个类 RingHomClass₃ 来扩展 MonoidHomClass₃ ，然后将其实例化为 RingHom ，之后再实例化为 AlgebraHom （代数是具有某些额外结构的环）。不过，我们已经涵盖了 Mathlib 中用于态射的主要形式化思想，您应该已经准备好理解 Mathlib 中态射的定义方式了。 作为练习，您应当尝试定义有序类型之间的保序函数类，以及保序幺半群同态。这仅用于训练目的。与连续函数类似，在 Mathlib 中保序函数主要是未打包的，它们通过 Monotone 预言来定义。当然，您需要完成下面的类定义。

@[ext]
structure OrderPresHom (α β : Type) [LE α] [LE β] where
  toFun : α → β
  le_of_le : ∀ a a', a ≤ a' → toFun a ≤ toFun a'

@[ext]
structure OrderPresMonoidHom (M N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends
MonoidHom₁ M N, OrderPresHom M N

class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β]

instance (α β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    OrderPresHomClass (OrderPresMonoidHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    MonoidHomClass₃ (OrderPresMonoidHom α β) α β
  := sorry

7.3. 子对象

定义了一些代数结构及其态射之后，下一步是考虑继承这种代数结构的集合，例如子群或子环。 这在很大程度上与我们之前的话题重叠。实际上， X 中的一个集合是作为从 X 到 Prop 的函数来实现的，因此子对象是满足特定谓词的函数。 因此，我们可以重用许多导致 DFunLike 类及其后代的想法。 我们不会重用 DFunLike 本身，因为这会破坏从 Set X 到 X → Prop 的抽象屏障。取而代之的是有一个 SetLike 类。该类不是将一个嵌入包装到函数类型中，而是将其包装到 Set 类型中，并定义相应的强制转换和 Membership 实例。

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

/-- `M` 中的子幺半群可以被视为 `M` 中的集合 -/
instance [Monoid M] : SetLike (Submonoid₁ M) M where
  coe := Submonoid₁.carrier
  coe_injective' _ _ := Submonoid₁.ext

借助上述的 SetLike 实例，我们已经可以很自然地表述子幺半群 N 包含 1 ，而无需使用 N.carrier 。 我们还可以将 N 作为 M 中的一个集合来处理，或者在映射下取其直接像。

example [Monoid M] (N : Submonoid₁ M) : 1 ∈ N := N.one_mem

example [Monoid M] (N : Submonoid₁ M) (α : Type) (f : M → α) := f '' N

我们还有一个到 Type 的强制转换，它使用 Subtype ，因此，给定一个子幺半群 N ，我们可以写一个参数 (x : N) ，其可以被强制转换为属于 N 的 M 的一个元素。

example [Monoid M] (N : Submonoid₁ M) (x : N) : (x : M) ∈ N := x.property

利用这种到 Type 的强制转换，我们还可以解决为子幺半群配备幺半群结构的任务。我们将使用上述与 N 相关联的类型的强制转换，以及断言这种强制转换是单射的引理 SetCoe.ext 。这两者均由 SetLike 实例提供。

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))

请注意，在上述实例中，我们本可以使用解构绑定器，而不是使用到 M 的强制转换并调用 property 字段，如下所示。

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

为了将关于子幺半群的引理应用于子群或子环，我们需要一个类，就像对于同态一样。请注意，这个类将一个 SetLike 实例作为参数，因此它不需要载体字段，并且可以在其字段中使用成员符号。

class SubmonoidClass₁ (S : Type) (M : Type) [Monoid M] [SetLike S M] : Prop where
  mul_mem : ∀ (s : S) {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
  one_mem : ∀ s : S, 1 ∈ s

instance [Monoid M] : SubmonoidClass₁ (Submonoid₁ M) M where
  mul_mem := Submonoid₁.mul_mem
  one_mem := Submonoid₁.one_mem

作为练习，您应该定义一个 Subgroup₁ 结构，为其赋予一个 SetLike 实例和一个 SubmonoidClass₁ 实例，在与 Subgroup₁ 相关联的子类型上放置一个 Group 实例，并定义一个 SubgroupClass₁ 类。

在 Mathlib 中，关于给定代数对象的子对象，还有一点非常重要，那就是它们总是构成一个完备格，这种结构被大量使用。例如，您可能会寻找一个关于子幺半群交集仍是子幺半群的引理。但这不会是一个引理，而是一个下确界构造。我们来看两个子幺半群的情况。

instance [Monoid M] : Inf (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'⟩ }⟩

这使得两个子幺半群的交集能够作为一个子幺半群得到。

example [Monoid M] (N P : Submonoid₁ M) : Submonoid₁ M := N ⊓ P

您可能会觉得在上面的例子中使用下确界符号 ⊓ 而不是交集符号 ∩ 很遗憾。但想想上确界。两个子幺半群的并集不是子幺半群。然而，子幺半群仍然构成一个格（甚至是完备格）。实际上， N ⊔ P 是由 N 和 P 的并集生成的子幺半群，当然用 N ∪ P 来表示会非常令人困惑。所以您可以看到使用 N ⊓ P 要一致得多。在各种代数结构中，这种表示法也更加一致。一开始看到两个子空间 E 和 F 的和用 E ⊔ F 而不是 E + F 表示可能会觉得有点奇怪。但您会习惯的。很快你就会觉得 E + F 这种表示法是一种干扰，它强调的是一个偶然的事实，即 E ⊔ F 的元素可以写成 E 的一个元素与 F 的一个元素之和，而不是强调 E ⊔ F 是包含 E 和 F 的最小向量子空间这一根本事实。

本章的最后一个主题是商的概念。同样，我们想要解释在 Mathlib 中如何构建方便的符号表示法以及如何避免代码重复。这里的主要手段是 HasQuotient 类，它允许使用诸如 M ⧸ N 这样的符号表示法。请注意，商符号 ⧸ 是一个特殊的 Unicode 字符，而不是普通的 ASCII 除法符号。

例如，我们将通过一个子幺半群来构建一个交换幺半群的商，证明留给你。在最后一个示例中，您可以使用 Setoid.refl ，但它不会自动获取相关的 Setoid 结构。您可以使用 @ 语法提供所有参数来解决此问题，例如 @Setoid.refl M 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
  }

instance [CommMonoid M] : HasQuotient M (Submonoid M) where
  quotient' := fun N ↦ Quotient N.Setoid

def QuotientMonoid.mk [CommMonoid M] (N : Submonoid M) : M → M ⧸ N := Quotient.mk N.Setoid

instance [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N) where
  mul := Quotient.map₂' (· * ·) (by
      sorry
        )
  mul_assoc := by
      sorry
  one := QuotientMonoid.mk N 1
  one_mul := by
      sorry
  mul_one := by
      sorry