论文标题

在lambek嵌入和产品保存的预设类别上

On the Lambek embedding and the category of product-preserving presheaves

论文作者

Fu, Peng, Kishida, Kohei, Ross, Neil J., Selinger, Peter

论文摘要

众所周知,Presheaf函子的类别是完整且合并的,并且Yoneda嵌入到Presheaf类别中可以保留产品。但是,YONEDA嵌入不保留相关。也许还不众所周知,如果我们将Yoneda嵌入Yoneda的代码量限制为限制性功能子的完整子类别,那么这将嵌入保留colimits,同时仍然享受Yoneda嵌入的大多数其他有用的属性。我们称此修改后的嵌入Lambek嵌入。众所周知,限制函数的类别是所有函子类别的反射子类别,即包含函数有一个左侧的伴随。在文献中,这种左伴随的存在通常是非结构性证明的,例如,通过弗雷德的伴随函子定理的应用。在本文中,我们为这一事实提供了一种替代性,更具建设性的证明。我们首先解释了Lambek的嵌入以及为什么保留共同的嵌入。然后,我们回顾了来自多组代数的一些概念,并观察到产品保存的预状态与某些多组术语代数之间存在一对一的对应关系。我们提供了一种将任何前膜函数变成产品保护的结构,因此给出了包含的左伴函数的明确定义。最后,我们素描如何扩展我们的方法,以证明极限限制函数的子类别也反映了。

It is well-known that the category of presheaf functors is complete and cocomplete, and that the Yoneda embedding into the presheaf category preserves products. However, the Yoneda embedding does not preserve coproducts. It is perhaps less well-known that if we restrict the codomain of the Yoneda embedding to the full subcategory of limit-preserving functors, then this embedding preserves colimits, while still enjoying most of the other useful properties of the Yoneda embedding. We call this modified embedding the Lambek embedding. The category of limit-preserving functors is known to be a reflective subcategory of the category of all functors, i.e., there is a left adjoint for the inclusion functor. In the literature, the existence of this left adjoint is often proved non-constructively, e.g., by an application of Freyd's adjoint functor theorem. In this paper, we provide an alternative, more constructive proof of this fact. We first explain the Lambek embedding and why it preserves coproducts. Then we review some concepts from multi-sorted algebras and observe that there is a one-to-one correspondence between product-preserving presheaves and certain multi-sorted term algebras. We provide a construction that freely turns any presheaf functor into a product-preserving one, hence giving an explicit definition of the left adjoint functor of the inclusion. Finally, we sketch how to extend our method to prove that the subcategory of limit-preserving functors is also reflective.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源