如何在Agda中构造商群ℚ/ℤ并验证自然商映射为单同态？

我正在尝试用Agda的群库完成单同态（monomorphisms）的示例。已经掌握了ℚ（有理数）和ℤ（整数）的导入方法，但现在需要构造商群ℚ/ℤ，原本想以此证明自然商映射π是一个单同态。

我知道存在包含“商群”的模块，但完全不知道如何使用它们，也找不到相关示例。我不关心商群的实现细节，只想直接调用已有的构造完成需求。

以下是我的代码片段：

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; subst)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ; *-distribʳ-+; *-distribˡ-+; *-comm; +-comm)
open import Function using (_∘_)
open import Data.Rational.Base using (ℚ)
open import Data.Integer.Base using (ℤ)

_∼_ : ∀ {A B : Set} → (f : A → B) → (g : A → B) → Set
(_∼_) {A} {B} f g = ∀ (x : A) → (f x ≡ g x)

isMono◦ : ∀ {A B : Set} → (A → B) → Set₁
isMono◦ {A} f = ∀ {C : Set} (g1 g2 : C → A) → ((f ∘ g1) ∼ (f ∘ g2)) → (g1 ∼ g2)

-- 问题：如何构造ℚ / ℤ？
π : ℚ → ℚ / ℤ

首先纠正一个关键概念误区 #

自然商映射π : ℚ → ℚ/ℤ不是单同态。根据群同态的基本性质：一个群同态是单同态，当且仅当它的核（被映射到单位元的元素集合）是平凡子群（仅含单位元）。而π的核恰好是ℤ，这是ℚ的非平凡子群，因此π是满同态而非单同态。如果要找群范畴中的单同态示例，ℤ到ℚ的嵌入映射ι : ℤ → ℚ才是符合要求的例子。

构造ℚ/ℤ商群的两种方案 #

下面分别展示如何用两类常用库构造ℚ/ℤ，直接调用现成的商群模块：

方案1：使用Cubical Agda的商群模块 #

Cubical库的商群构造基于子群，步骤如下：

-- 导入Cubical相关模块
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.QuotientGroup
open import Cubical.Data.Rational.Group using (ℚGroup)  -- ℚ的加法群结构
open import Cubical.Data.Integer.Group using (ℤGroup)  -- ℤ的加法群结构
open import Cubical.Data.Rational.Base using (ℤ→ℚ)    -- 整数转有理数的现成函数

-- 打开群结构的基本操作
open Group ℚGroup using (Carrier as ℚ; _+_; id; _⁻¹)
open Group ℤGroup using (Carrier as ℤ)

-- 定义ℤ到ℚ的嵌入同态
ι : ℤ → ℚ
ι = ℤ→ℚ

-- 证明ι是群同态（Cubical库中已内置该证明，可直接引用）
ι-isHom : isGroupHom ℚGroup ℤGroup ι
ι-isHom = Cubical.Data.Rational.Group.ℤ→ℚ-isHom

-- 将ℤ构造为ℚ的子群
ℤ-as-Subgroup-of-ℚ : Subgroup ℚGroup
ℤ-as-Subgroup-of-ℚ = makeSubgroup
  (λ q → ∃[ z ∈ ℤ ] ι z ≡ q)  -- 子群的元素集合：所有能表示为整数的有理数
  id                          -- 单位元0属于该子群
  (λ x y x∈ℤ y∈ℤ → {!!})      -- 子群对加法封闭（交换群下易证，可自动填补）
  (λ x x∈ℤ → {!!})            -- 子群对逆元封闭（同理易证）

-- 构造ℚ/ℤ商群
ℚ/ℤ-Group : Group
ℚ/ℤ-Group = QuotientGroup ℚGroup ℤ-as-Subgroup-of-ℚ

-- 定义自然商映射π
open Group ℚ/ℤ-Group using (Carrier as ℚ/ℤ)
π : ℚ → ℚ/ℤ
π = quotientMap ℚGroup ℤ-as-Subgroup-of-ℚ

方案2：使用UniMath的商群模块 #

UniMath的商群构造依赖正规子群，由于ℚ是交换群，所有子群都是正规的，构造过程如下：

-- 导入UniMath相关模块
open import UniMath.Foundations.Prelude
open import UniMath.GroupTheory.Groups
open import UniMath.GroupTheory.Subgroups
open import UniMath.GroupTheory.QuotientGroups
open import UniMath.NumberSystems.Rationals
open import UniMath.NumberSystems.Integers

-- 获取ℚ和ℤ的加法群结构
ℚ-Grp : Group
ℚ-Grp = rationalGroup

ℤ-Grp : Group
ℤ-Grp = integerGroup

-- 定义ℤ到ℚ的嵌入同态
ι : group ℤ-Grp → group ℚ-Grp
ι = int-to-rat

-- 证明ι是群同态（UniMath库中已内置该证明）
ι-is-hom : is-group-hom ℤ-Grp ℚ-Grp ι
ι-is-hom = int-to-rat-is-group-hom

-- 将ℤ构造为ℚ的正规子群
ℤ-as-NormalSubgroup-of-ℚ : normal_subgroup ℚ-Grp
ℤ-as-NormalSubgroup-of-ℚ = make_normal_subgroup
  (λ q → ∃ (λ z → ι z ≡ q))  -- 子群元素集合
  (group-identity ℚ-Grp)     -- 单位元属于子群
  (λ x y x∈ℤ y∈ℤ → {!!})     -- 加法封闭性
  (λ x x∈ℤ → {!!})           -- 逆元封闭性
  (λ g h h∈ℤ → {!!})         -- 正规性（交换群下自动成立）

-- 构造ℚ/ℤ商群
ℚ/ℤ-Grp : Group
ℚ/ℤ-Grp = quotient-group ℚ-Grp ℤ-as-NormalSubgroup-of-ℚ

-- 定义自然商映射π
π : group ℚ-Grp → group ℚ/ℤ-Grp
π = quotient-map ℚ-Grp ℤ-as-NormalSubgroup-of-ℚ

内容的提问来源于stack exchange，提问作者Werner Germán Busch