Pith. sign in

REVIEW 2 cited by

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

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2205.06068 v1 pith:544BHQDP submitted 2022-05-12 math.CT cs.LO

classification math.CTcs.LO
keywords embeddingcategoryfunctorsadjointfunctoryonedalambekleft
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Logical relations for call-by-push-value models, via internal fibrations in a 2-category

    cs.LO 2025-05 conditional novelty 7.0 of 10

    A 2-categorical fibrational framework gives a uniform notion of logical relations for CBPV models, with a pullback theorem that constructs new relational models from old ones.

  2. Quantalic lambda-calculus and additive disjunction

    cs.LO 2026-08 conditional novelty 6.0 of 10

    Quantalic linear lambda-calculus gains an additive disjunction operator with sound and approximately complete equational reasoning, plus probabilistic and quantum model constructions.

Pith tools