Groupoids

Author: Trebor-Huang

examples.typ

@@ -27,7 +27,7 @@
 若要用有向图构建模型，就需要定义依值有向图的概念。
 #definition[
   给定有向图 $Gamma$，*依值有向图*包含如下资料：对于每个顶点 $x in Gamma$，有一族集合 $V_x$ 表示依值顶点，对于每条边 $e : x -> y$，有一族集合 $E_e$ 表示依值边，配有两个函数 $s : E_e -> V_x$ 与 $t : E_e -> V_y$。其中的元素写作 $epsilon : alpha xarrow(e) beta$.
-]
+] <def:dependent-graph>
 不难看出，依值有向图就是依值集合 —— 即集合族 —— 的简单推广。给定有向图 $Gamma$ 与依值有向图 $A$，可以将 $A$ 中的所有顶点与边合在一起构成新的有向图 $integral A$，称作*全图*。其顶点形如 $(x, y)$，其中 $x$ 是 $Gamma$ 的顶点，而 $y$ 是关于 $x$ 的依值顶点。类似地，其边形如 $(e, epsilon)$。这条边的起点和终点分别是 $(s(e), s(epsilon))$ 与 $(t(e), t(epsilon))$。这构成语境扩展 $(Gamma, A)$ 的解释。请读者构造图同态 $frak(p) : integral A -> Gamma$。
 
 #numbered-figure(caption: [依值有向图], placement: auto)[
@@ -288,13 +288,43 @@ $)
 
 同伦意义下的空间结构十分丰富，因此要直接以空间构造出类型论的模型有些难度。我们将其推迟到#[@ch:homotopy-theory]。Hofmann 与 Streicher 则采用了只能记录一部分同伦信息的数学结构，对空间做粗略的近似。这个数学结构就是#translate[群胚][groupoid]。
 
-- Intuition of paths and spaces
-- Start with directed graphs
+#definition[
+  *群胚* $G$ 包含一些点 $x, y in G$ 的集合，两点之间有道路集 $hom_G (x, y)$，
+  - 道路有拼接操作，将 $p in hom_G (x, y)$ 与 $q in hom_G (y, z)$ 拼接为 $q * p in hom_G (x, z)$。
+  - 有平凡道路 $"refl"(x) in hom_G (x, x)$。
+  - 拼接操作满足结合律 $(p * q) * r = p * (q * r)$ 与单位律 $"refl"(y) * p = p = p * "refl"(x)$。
+  - 道路有逆转操作，将 $p in hom_G (x, y)$ 变为 $p^(-1) in hom_G (y, x)$，满足 $p^(-1) * p = "refl"(x)$ 与 $p * p^(-1) = "refl"(y)$。
+] <def:groupoid>
+群胚的定义刻画了空间中的点与它们之间的道路，不过没有记录二维乃至更高维的结构信息。最常见的构造群胚的办法是给定一个空间，而后忘记二维以上的信息。这个构造称作基本群胚。
+#definition[
+  给定拓扑空间 $X$，可以定义*基本群胚* $pi_(<= 1) (X)$ 的点集为 $X$ 的点集，而 $hom_(pi_(<=1) (X)) (x, y)$ 为 $x$ 到 $y$ 的道路集合，商去同伦关系。 // 换句话说，其中的元素形如连续函数 $p : [0, 1] -> X$，使得 $p(0) = x$，$p(1) = y$。如果有两条道路 $p$ 与 $q$，使得存在连续函数 $H : [0, 1] times [0, 1] -> X$
+]
+如果不熟悉拓扑的基本概念也不要紧。两点之间的道路就是以它们为起点和终点的连续曲线。而如果两条连续曲线能在端点不移动的情况下连续地从一条变为另一条，就说它们同伦。不过，群胚的优点在于它将拓扑概念完全_代数化_了，因此可以简单地按照代数思维，或者离散的组合视角处理群胚，无需担心点集拓扑的技术细节。
+
+群胚的代数性在名字上就初见端倪。如果群胚只有一个点 $star$，那么 $star$ 到自己的道路集合构成一个群.#footnote[许多文献会因此称群是群胚的特殊情况，不过这并不好。群胚的 “元素” 集是它的点集，但群的元素在这个对应下却变成了道路 —— 由于是一个点到自己的道路，所以也叫做*环路* —— 的集合。这么看，这两个概念某种意义上相差了一个维度。因此，我们称一个群 $G$ 对应的群胚为#define[解环群胚][delooping groupoid]，写作 $"B"G$。] 其中群运算是道路拼接。
+例如，一般的魔方上的公式变换就构成一个群。群运算是将两个公式并排放置，而单位元是空公式。考虑一种常见的魔方变体，将某些块粘在一起，禁止相对滑动，称作*捆绑魔方*。此时，由于某个状态下并不是所有转动都可以进行，有一些会被捆绑限制，因此它对应的代数结构就从群变成群胚。其中，每一个状态对应一个点，该状态下能执行的公式 (注意可以包括多步转动) 对应道路。由于所有公式都有逆公式，这的确构成群胚。
+
+另一个组合性质的例子是图上的道路。 (...)
 
-...... 1991 年，Воеводский (Voevodsky) 与合作者 Михаил Капранов (Mikhail Kapranov) 给出了一种无穷群胚的定义，并证明了这种无穷群胚能在同伦意义下表示所有的空间 [?]。但是 1998 年，由 Carlos Simpson~[?] 给出了反例，因此证明有误。事实上球面 $SS^2$ 就不在其表达能力范围内。然而，很长一段时间内，人们都没有明白错误在哪里，因此不清楚究竟是证明有误还是反例不成立。这件事是 Воеводский 转而追求形式化证明的动机之一。
+
+(a higher concept of groupoids that doesn't throw away information) ...... 1991 年，Воеводский (Voevodsky) 与合作者 Михаил Капранов (Mikhail Kapranov) 给出了一种无穷群胚的定义，并证明了这种无穷群胚能在同伦意义下表示所有的空间 [?]。但是 1998 年，由 Carlos Simpson~[?] 给出了反例，因此证明有误。事实上球面 $SS^2$ 就不在其表达能力范围内。然而，很长一段时间内，人们都没有明白错误在哪里，因此不清楚究竟是证明有误还是反例不成立。这件事是 Воеводский 转而追求形式化证明的动机之一。
 
 === 模型定义
 
+按照惯例，我们将语境解释为群胚，而类型解释为依值群胚，定义如下。
+#definition[
+  给定群胚 $Gamma$，定义*依值群胚* $A$ 包含如下资料：对于每个点 $x in Gamma$ 配备集合 $A_x$，对于每条道路 $p in hom_Gamma (x, y)$ 与 $alpha in A_x$ 和 $beta in A_y$ 配备道路集 $hom_A^p (alpha, beta)$。有平凡道路 $"refl"(alpha) in hom_A^("refl"(x)) (alpha, alpha)$、道路逆转 $(-)^(-1) : hom_A^p (alpha, beta) -> hom_A^(p^(-1)) (beta, alpha)$ 与道路拼接操作
+  #eq($ hom_A^p (y, z) times hom_A^q (x, y) -> hom_A^(p * q) (x, z), $)
+  满足单位律、结合律，并且道路逆转满足 $xi * xi^(-1) = "refl"(alpha)$ 与 $xi^(-1) * xi = "refl"(beta)$。
+]
+定义与依值有向图 (@def:dependent-graph) 类似，只不过这里还为群胚中的每个运算规定了对应的依值运算。
+
+- Sigma type
+- Pi type
+- Path type
+- Must verify J rule
+  - maybe it's equivalent to combination of smaller rules?
+
 === K 原理的反模型
 
 == 可计算性与模型