8. 群与环

我们已经在 Section 2.2 中学习过如何对群与环中的运算进行推理。在稍后的 Section 6.2 也领略过定义抽象代数结构的方法。这类结构诸如群，或是像高斯整环这样的具体示例。Chapter 7 中解释了 Mathlib 如何处理这些抽象结构的层级关系。

本章中，我们将更为详细地探讨群和环。由于 Mathlib 总在扩展中，我们没办法一应俱全， 但我们将为你给出使用相关库的切入点，并展示如何使用其中的核心概念。 这一章和 Chapter 7 有些重复，但在这里我们会集中于如何使用 Mathlib，而非探究其背后的设计理念。 因此，要理解本章中的一些例子，你可能需要回顾 Chapter 7。

8.1. 幺半群与群

8.1.1. 幺半群和同态

抽象代数课程往往会从群讲起，一步步推进到环、域直至向量空间。这样的做法常会为讨论环上的乘法这样并不来自于群结构的运算带来不必要的曲折：许多群中的定理的证明方法其实也能适用，但我们却要再证一遍。 一般来说，当你是对着书本学习数学时，一行 “以下留作习题” 便是多数作者解决此窘境的方法。不过，在 Lean 中，我们有另一种虽然不那么方便，但却更安全，更对形式化友好的方法：引入幺半群 (monoid)。

类型 M 上的 幺半群 是一个在内部具有结合律和单位元的复合法则。幺半群被引入的首要目的是同时涵盖群和环上的乘法结构。有些较为自然的例子：比如，自然数与加法就构成一个幺半群。

从实际应用的角度来说，你几乎可以忘记 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. Subgroups

就像群同态是一系列映射一样，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

One can be fully concrete and compute actual products of cycles. Below we use the #simp command, which calls the simp tactic on a given expression. The notation c[] is used to define a cyclic permutation. In the example, the result is a permutation of ℕ. One could use a type ascription such as (1 : Fin 5) on the first number appearing to make it a computation in Perm (Fin 5).

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

Another way to work with concrete groups is to use free groups and group presentations. The free group on a type α is FreeGroup α and the inclusion map is FreeGroup.of : α → FreeGroup α. For instance let us define a type S with three elements denoted by a, b and c, and the element ab⁻¹ of the corresponding free group.

section FreeGroup

inductive S | a | b | c

open S

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

Note that we gave the expected type of the definition so that Lean knows that .of means FreeGroup.of.

The universal property of free groups is embodied as the equivalence FreeGroup.lift. For example, let us define the group morphism from FreeGroup S to Perm (Fin 5) that sends a to c[1, 2, 3], b to c[2, 3, 1], and c to 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]

As a last concrete example, let us see how to define a group generated by a single element whose cube is one (so that group will be isomorphic to \(\mathbb{Z}/3\)) and build a morphism from that group to Perm (Fin 5).

As a type with exactly one element, we will use Unit whose only element is denoted by (). The function PresentedGroup takes a set of relations, i.e. a set of elements of some free group, and returns a group that is this free group quotiented by a normal subgroup generated by relations. (We will see how to handle more general quotients in Section 8.1.6.) Since we somehow hide this behind a definition, we use deriving Group to force creation of a group instance on myGroup.

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

The universal property of presented groups ensures that morphisms out of this group can be built from functions that send the relations to the neutral element of the target group. So we need such a function and a proof that the condition holds. Then we can feed this proof to PresentedGroup.toGroup to get the desired group morphism.

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. Group actions

One important way that group theory interacts with the rest of mathematics is through the use of group actions. An action of a group G on some type X is nothing more than a morphism from G to Equiv.Perm X. So in a sense group actions are already covered by the previous discussion. But we don’t want to carry this morphism around; instead, we want it to be inferred automatically by Lean as much as possible. So we have a type class for this, which is MulAction G X. The downside of this setup is that having multiple actions of the same group on the same type requires some contortions, such as defining type synonyms, each of which carries different type class instances.

This allows us in particular to use g • x to denote the action of a group element g on a point 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

There is also a version for additive group called AddAction, where the action is denoted by +ᵥ. This is used for instance in the definition of affine spaces.

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

The underlying group morphism is called MulAction.toPermHom.

open MulAction

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

As an illustration let us see how to define the Cayley isomorphism embedding of any group G into a permutation group, namely Perm G.

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

Note that nothing before the above definition required having a group rather than a monoid (or any type endowed with a multiplication operation really).

The group condition really enters the picture when we will want to partition X into orbits. The corresponding equivalence relation on X is called MulAction.orbitRel. It is not declared as a global instance.

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

Using this we can state that X is partitioned into orbits under the action of G. More precisely, we get a bijection between X and the dependent product (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) where Quotient.out' ω simply chooses an element that projects to ω. Recall that elements of this dependent product are pairs ⟨ω, x⟩ where the type orbit G (Quotient.out' ω) of x depends on ω.

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

In particular, when X is finite, this can be combined with Fintype.card_congr and Fintype.card_sigma to deduce that the cardinality of X is the sum of the cardinalities of the orbits. Furthermore, the orbits are in bijection with the quotient of G under the action of the stabilizers by left translation. This action of a subgroup by left-translation is used to define quotients of a group by a subgroup with notation / so we can use the following concise statement.

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

An important special case of combining the above two results is when X is a group G equipped with the action of a subgroup H by translation. In this case all stabilizers are trivial so every orbit is in bijection with H and we get:

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

This is the conceptual variant of the version of Lagrange theorem that we saw above. Note this version makes no finiteness assumption.

As an exercise for this section, let us build the action of a group on its subgroup by conjugation, using our definition of conjugate from a previous exercise.

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. Quotient groups

In the above discussion of subgroups acting on groups, we saw the quotient G ⧸ H appear. In general this is only a type. It can be endowed with a group structure such that the quotient map is a group morphism if and only if H is a normal subgroup (and this group structure is then unique).

The normality assumption is a type class Subgroup.Normal so that type class inference can use it to derive the group structure on the quotient.

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

The universal property of quotient groups is accessed through QuotientGroup.lift: a group morphism φ descends to G ⧸ N as soon as its kernel contains 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

The fact that the target group is called M is the above snippet is a clue that having a monoid structure on M would be enough.

An important special case is when N = ker φ. In that case the descended morphism is injective and we get a group isomorphism onto its image. This result is often called the first isomorphism theorem.

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

Applying the universal property to a composition of a morphism φ : G →* G' with a quotient group projection Quotient.mk' N', we can also aim for a morphism from G ⧸ N to G' ⧸ N'. The condition required on φ is usually formulated by saying “φ should send N inside N'.” But this is equivalent to asking that φ should pull N' back over N, and the latter condition is nicer to work with since the definition of pullback does not involve an existential quantifier.

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

One subtle point to keep in mind is that the type G ⧸ N really depends on N (up to definitional equality), so having a proof that two normal subgroups N and M are equal is not enough to make the corresponding quotients equal. However the universal properties does give an isomorphism in this case.

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

As a final series of exercises for this section, we will prove that if H and K are disjoint normal subgroups of a finite group G such that the product of their cardinalities is equal to the cardinality of G then G is isomorphic to H × K. Recall that disjoint in this context means H ⊓ K = ⊥.

We start with playing a bit with Lagrange’s lemma, without assuming the subgroups are normal or disjoint.

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

open MonoidHom

#check Nat.card_pos -- The nonempty argument will be automatically inferred for subgroups
#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

From now on, we assume that our subgroups are normal and disjoint, and we assume the cardinality condition. Now we construct the first building block of the desired isomorphism.

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

Now we can define our second building block. We will need MonoidHom.prod, which builds a morphism from G₀ to G₁ × G₂ out of morphisms from G₀ to G₁ and G₂.

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

We are ready to put all pieces together.

#check MulEquiv.prodCongr

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

8.2. Rings

8.2.1. Rings, their units, morphisms and subrings

The type of ring structures on a type R is Ring R. The variant where multiplication is assumed to be commutative is CommRing R. We have already seen that the ring tactic will prove any equality that follows from the axioms of a commutative ring.

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

More exotic variants do not require that the addition on R forms a group but only an additive monoid. The corresponding type classes are Semiring R and CommSemiring R. The type of natural numbers is an important instance of CommSemiring R, as is any type of functions taking values in the natural numbers. Another important example is the type of ideals in a ring, which will be discussed below. The name of the ring tactic is doubly misleading, since it assumes commutativity but works in semirings as well. In other words, it applies to any CommSemiring.

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

There are also versions of the ring and semiring classes that do not assume the existence of a multiplicative unit or the associativity of multiplication. We will not discuss those here.

Some concepts that are traditionally taught in an introduction to ring theory are actually about the underlying multiplicative monoid. A prominent example is the definition of the units of a ring. Every (multiplicative) monoid M has a predicate IsUnit : M → Prop asserting existence of a two-sided inverse, a type Units M of units with notation Mˣ, and a coercion to M. The type Units M bundles an invertible element with its inverse as well as properties than ensure that each is indeed the inverse of the other. This implementation detail is relevant mainly when defining computable functions. In most situations one can use IsUnit.unit {x : M} : IsUnit x → Mˣ to build a unit. In the commutative case, one also has Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ which builds x seen as unit.

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

The type of ring morphisms between two (semi)-rings R and S is RingHom R S, with notation 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

The isomorphism variant is RingEquiv, with notation ≃+*.

As with submonoids and subgroups, there is a Subring R type for subrings of a ring R, but this type is a lot less useful than the type of subgroups since one cannot quotient a ring by a subring.

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

Also notice that RingHom.range produces a subring.

8.2.2. Ideals and quotients

For historical reasons, Mathlib only has a theory of ideals for commutative rings. (The ring library was originally developed to make quick progress toward the foundations of modern algebraic geometry.) So in this section we will work with commutative (semi)rings. Ideals of R are defined as submodules of R seen as R-modules. Modules will be covered later in a chapter on linear algebra, but this implementation detail can mostly be safely ignored since most (but not all) relevant lemmas are restated in the special context of ideals. But anonymous projection notation won’t always work as expected. For instance, one cannot replace Ideal.Quotient.mk I by I.Quotient.mk in the snippet below because there are two .``s and so it will parse as ``(Ideal.Quotient I).mk; but Ideal.Quotient by itself doesn’t exist.

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

The universal property of quotient rings is 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

In particular it leads to the first isomorphism theorem for rings.

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

Ideals form a complete lattice structure with the inclusion relation, as well as a semiring structure. These two structures interact nicely.

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

One can use ring morphisms to push ideals forward and pull them back using Ideal.map and Ideal.comap, respectively. As usual, the latter is more convenient to use since it does not involve an existential quantifier. This explains why it is used to state the condition that allows us to build morphisms between quotient rings.

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

One subtle point is that the type R ⧸ I really depends on I (up to definitional equality), so having a proof that two ideals I and J are equal is not enough to make the corresponding quotients equal. However, the universal properties do provide an isomorphism in this case.

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

We can now present the Chinese remainder isomorphism as an example. Pay attention to the difference between the indexed infimum symbol ⨅ and the big product of types symbol Π. Depending on your font, those can be pretty hard to distinguish.

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

The elementary version of the Chinese remainder theorem, a statement about ZMod, can be easily deduced from the previous one:

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

As a series of exercises, we will reprove the Chinese remainder theorem in the general case.

We first need to define the map appearing in the theorem, as a ring morphism, using the universal property of quotient rings.

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

#check Pi.ringHom
#check ker_Pi_Quotient_mk

/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
  Remainder Theorem. -/
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  sorry

Make sure the following next two lemmas can be proven by 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

The next lemma proves the easy half of the Chinese remainder theorem, without any assumption on the family of ideals. The proof is less than one line long.

#check injective_lift_iff

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

We are now ready for the heart of the theorem, which will show the surjectivity of our chineseMap. First we need to know the different ways one can express the coprimality (also called co-maximality assumption). Only the first two will be needed below.

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

We take the opportunity to use induction on Finset. Relevant lemmas on Finset are given below. Remember that the ring tactic works for semirings and that the ideals of a ring form a semiring.

#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

We can now prove surjectivity of the map appearing in the Chinese remainder theorem.

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

Now all the pieces come together in the following:

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. Algebras and polynomials

Given a commutative (semi)ring R, an algebra over R is a semiring A equipped with a ring morphism whose image commutes with every element of A. This is encoded as a type class Algebra R A. The morphism from R to A is called the structure map and is denoted algebraMap R A : R →+* A in Lean. Multiplication of a : A by algebraMap R A r for some r : R is called the scalar multiplication of a by r and denoted by r • a. Note that this notion of algebra is sometimes called an associative unital algebra to emphasize the existence of more general notions of algebra.

The fact that algebraMap R A is ring morphism packages together a lot of properties of scalar multiplication, such as the following:

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

The morphisms between two R-algebras A and B are ring morphisms which commute with scalar multiplication by elements of R. They are bundled morphisms with type AlgHom R A B, which is denoted by A →ₐ[R] B.

Important examples of non-commutative algebras include algebras of endomorphisms and algebras of square matrices, both of which will be covered in the chapter on linear algebra. In this chapter we will discuss one of the most important examples of a commutative algebra, namely, polynomial algebras.

The algebra of univariate polynomials with coefficients in R is called Polynomial R, which can be written as R[X] as soon as one opens the Polynomial namespace. The algebra structure map from R to R[X] is denoted by C, which stands for “constant” since the corresponding polynomial functions are always constant. The indeterminate is denoted by X.

open Polynomial

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

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

In the first example above, it is crucial that we give Lean the expected type since it cannot be determined from the body of the definition. In the second example, the target polynomial algebra can be inferred from our use of C r since the type of r is known.

Because C is a ring morphism from R to R[X], we can use all ring morphisms lemmas such as map_zero, map_one, map_mul, and map_pow before computing in the ring R[X]. For example:

example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
  rw [C.map_pow]
  ring

You can access coefficients using 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

Defining the degree of a polynomial is always tricky because of the special case of the zero polynomial. Mathlib has two variants: Polynomial.natDegree : R[X] → ℕ assigns degree 0 to the zero polynomial, and Polynomial.degree : R[X] → WithBot ℕ assigns ⊥. In the latter, WithBot ℕ can be seen as ℕ ∪ {-∞}, except that -∞ is denoted ⊥, the same symbol as the bottom element in a complete lattice. This special value is used as the degree of the zero polynomial, and it is absorbent for addition. (It is almost absorbent for multiplication, except that ⊥ * 0 = 0.)

Morally speaking, the degree version is the correct one. For instance, it allows us to state the expected formula for the degree of a product (assuming the base ring has no zero divisor).

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

Whereas the version for natDegree needs to assume non-zero polynomials.

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

However, ℕ is much nicer to use than WithBot ℕ, so Mathlib makes both versions available and provides lemmas to convert between them. Also, natDegree is the more convenient definition to use when computing the degree of a composition. Composition of polynomial is Polynomial.comp and we have:

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

Polynomials give rise to polynomial functions: any polynomial can be evaluated on R using Polynomial.eval.

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

In particular, there is a predicate, IsRoot, that holds for elements r in R where a polynomial vanishes.

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

We would like to say that, assuming R has no zero divisor, a polynomial has at most as many roots as its degree, where the roots are counted with multiplicities. But once again the case of the zero polynomial is painful. So Mathlib defines Polynomial.roots to send a polynomial P to a multiset, i.e. the finite set that is defined to be empty if P is zero and the roots of P, with multiplicities, otherwise. This is defined only when the underlying ring is a domain since otherwise the definition does not have good properties.

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

Both Polynomial.eval and Polynomial.roots consider only the coefficients ring. They do not allow us to say that X ^ 2 - 2 : ℚ[X] has a root in ℝ or that X ^ 2 + 1 : ℝ[X] has a root in ℂ. For this, we need Polynomial.aeval, which will evaluate P : R[X] in any R-algebra. More precisely, given a semiring A and an instance of Algebra R A, Polynomial.aeval sends every element of a along the R-algebra morphism of evaluation at a. Since AlgHom has a coercion to functions, one can apply it to a polynomial. But aeval does not have a polynomial as an argument, so one cannot use dot notation like in P.eval above.

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

The function corresponding to roots in this context is aroots which takes a polynomial and then an algebra and outputs a multiset (with the same caveat about the zero polynomial as for 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 knows about D'Alembert-Gauss theorem: ``ℂ`` is algebraically closed.
example : IsAlgClosed ℂ := inferInstance

More generally, given an ring morphism f : R →+* S one can evaluate P : R[X] at a point in S using Polynomial.eval₂. This one produces an actual function from R[X] to S since it does not assume the existence of a Algebra R S instance, so dot notation works as you would expect.

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

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

Let us end by mentioning multivariate polynomials briefly. Given a commutative semiring R, the R-algebra of polynomials with coefficients in R and indeterminates indexed by a type σ is MVPolynomial σ R. Given i : σ, the corresponding polynomial is MvPolynomial.X i. (As usual, one can open the MVPolynomial namespace to shorten this to X i.) For instance, if we want two indeterminates we can use Fin 2 as σ and write the polynomial defining the unit circle in \(\mathbb{R}^2`\) as:

open MvPolynomial

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

Recall that function application has a very high precedence so the expression above is read as (X 0) ^ 2 + (X 1) ^ 2 - 1. We can evaluate it to make sure the point with coordinates \((1, 0)\) is on the circle. Recall the ![...] notation denotes elements of Fin n → X for some natural number n determined by the number of arguments and some type X determined by the type of arguments.

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