依值和

在范畴论中, 依值和是一种万有构造, 是积的推广, 允许两个分量中有依赖关系.

1定义

依值和可以直接定义, 也可以用万有性质定义.

定义 1.1 (直接定义). 在范畴 $\mathcal{C}$ 中, 顺着态射 $f\in \mathcal{C}(A,I)$ 取的依值和是如下俯范畴间的函子: $$\begin{array}{rl}& {\sum }_f:{\mathcal{C}}_{/A}\to {\mathcal{C}}_{/I}\\ & {\sum }_f(g):=f\circ g\end{array}$$

定义 1.2 (万有性质). 令范畴 $\mathcal{C}$ 有所有的拉回, 换言之存在一函子 $f^{\ast }$ 进行 “顺着 $f$ 拉回” 的操作, 行为如下图所示: $$\bullet \bullet BA输出f^{\ast }(g)┌输入gf$$那么顺着态射 $f\in \mathcal{C}(A,I)$ 取的依值和是 $f^{\ast }$ 函子的左伴随.

2性质

3相关概念

•	局部积闭范畴中的伴随三元组中有依值和.

•	类型论中的$\Sigma$ 类型的范畴语义和依值和有关.

术语翻译

依值和 • 英文 dependent sum