Wiki. 截断性 [截断性]
Wiki. 截断性 [截断性]
观念
定义
固定一个 $\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)$-截断的.
通过局部性定义
定义 $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$: