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

TL;DR

This paper introduces a constructive approach to the Lambek embedding, showing how to explicitly obtain the left adjoint for the subcategory of limit-preserving functors, enhancing understanding of presheaf categories.

Contribution

It provides a constructive proof for the existence of the left adjoint to the inclusion of limit-preserving functors, using multi-sorted algebra concepts.

Findings

Explicit construction of the left adjoint functor.

Demonstration that the subcategory of limit-preserving functors is reflective.

Extension of the method to broader classes of functors.

Abstract

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.