路径归纳 [路径归纳]

百科
SimplicialCat

关联页面

单点 (同伦类型论) [单点(同伦类型论)]

百科
同伦类型论
SimplicialCat

定义

单点是同伦类型论中零个类型的乘积. 只有一种方式构造类型 $\mathbf 1$ 的元素:

$\star\colon \mathbf 1$.

性质

命题. 对任意 $x,y\colon \mathbf 1$, 有 $(x=y)\simeq\mathbf 1$.

证明. 首先, 有明显的映射 $(x=y)\to 1$ 将一切映射到 $\star$. 另一方面, 对于 $x,y\colon 1$, 由高阶归纳类型, 不妨设 $x\equiv \star$, $y\equiv \star$. 那么我们有 $\mathsf {refl}_{\star}\colon x=y$. 这给出一个映射 $1 \to (x=y)$.

我们证明上述两个映射互逆.

$\mathbf 1\to (x=y)\to \mathbf 1$, 考虑 $u\colon \mathbf 1$, 不妨设 $u\equiv\star$. 这说明这个复合是恒等.
$(x=y)\to\mathbf 1\to(x=y)$. 考虑 $p\colon (x=y)$, 由路径归纳, 不妨设 $x\equiv y$ 且 $p\equiv\mathsf {refl}_x$. 那么又不妨设 $x\equiv\star$. 此时复合映射将 $p$ 映射到 $\mathsf {refl}_x$, 也即 $p$ 自身.

推论. $\mathbf 1$ 是集合.

截断性 [截断性]

百科
SimplicialCat

观念

定义

固定一个 $\infty$-意象 (或更一般的可表现范畴) $\mathcal C$, 例如生象的范畴 $\mathsf{Ani}$.

归纳定义

我们对 $n\geq -2$ 归纳定义 $\mathcal X$ 中的对象和态射的 $n$-截断性. 态射 $X\to Y$ $n$-截断就是指其在俯意象 $\mathcal C_{/Y}$ 中是 $n$-截断对象.

$n=-2$:

$(-2)$-截断对象就是终对象 $*$.
$(-2)$-截断态射就是等价.

$n\geq -1$:

对象 $X$ 是 $n$-截断对象当且仅当对角线 $\Delta_X\colon X\to X\times X$ 是 $(n-1)$-截断态射.
态射 $f\colon X\to Y$ 是 $n$-截断态射当且仅当其在 $\mathcal C_{/Y}$ 中是 $n$-截断对象, 即 $\Delta_f \colon X \to X\times_Y X$ 是 $(n-1)$-截断态射.

$n$-截断的归纳定义是如下同伦类型论 (见截断性 (同伦类型论)) 命题的范畴语义: $X$ 是 $n$-截断的, 当且仅当对任意 $a,b \in X$, $$ a =_X b $$ 是 $(n-1)$-截断的.

通过环路空间定义

对于 $\mathsf{Ani}$ 的对象, 即生象 $X$, 还有另一种等价的归纳定义:

$X$ 是 $(-2)$-截断生象当且仅当 $X=1$;
$X$ 是 $(-1)$-截断生象当且仅当 $\Delta_X$ 是等价;
对于 $n\geq 0$ (注意必须从 $0$ 而不是 $-1$ 开始), $X$ 是 $n$-截断生象当且仅当对任意点 $x\in X$, 环路空间 $\Omega_x X$ 是 $(n-1)$-截断生象.

在一般的意象中, 使用广义点也可实现上述定义. 对于广义点 $x\colon U\to X$, 有 $\Omega_xX= U\times_X U$.

这个事实的证明可以使用同伦类型论中的路径归纳.

通过局部性定义

定义 $n$-截断对象为关于如下态射族的局部对象: $$ \{A\times S^{n+1} \to A\}. $$ 其中 $S^{n+1}$ 是 $(n+1)$ 维球面.

$n$-截断的局部对象定义是如下同伦类型论命题的范畴语义: $X$ 是 $n$-截断的, 当且仅当任意映射 $S^n \to X$ 都穿过某一个点 $x\in X$. 注意这句话不能在外部 (通常) 语言中理解.

同伦类型论

见截断性 (同伦类型论).

例

$n=-1$:

$(-1)$-截断对象就是子终对象, 又称真值.
$(-1)$-截断态射就是单射.