Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: co/yoneda as co/evaluation

Christian Williams (Apr 15 2021 at 03:46):

Let $F:C\to Set$ be a covariant $C$-module ("copresheaf").
The coYoneda lemma is left extension along the identity: $F \simeq \int^c F(c)\times C(c,-)$.
The Yoneda lemma is right extension along the identity: $\int_c [C(-,c),F(c)] \simeq F$.

Christian Williams (Apr 15 2021 at 03:47):

coYoneda characterizes a $C$-module as an indexed sum of representables.
Yoneda characterizes a $C$-module as an indexed product of representables.

Christian Williams (Apr 15 2021 at 03:48):

Because extensions are defined by adjunctions, these natural isomorphisms are actually a unit and counit.

Christian Williams (Apr 15 2021 at 03:49):

In some dream of generalized logic, I imagine these to be a fundamental form of $\eta$-expansion and $\beta$-reduction.

Christian Williams (Apr 15 2021 at 03:52):

we could write these in different styles.
$\mathtt{F = \Sigma c. Fc \times C(c,-)}$
$\mathtt{\Pi c. C(-,c)\to Fc = F}$

Christian Williams (Apr 15 2021 at 03:55):

I feel like this basic idea is sunk into many formal categorical proofs. But I don't know if I've seen this terminology explicitly.

Christian Williams (Apr 15 2021 at 03:56):

I think the analogy between $\eta$-expansion / $\beta$-reduction and co/Yoneda can be justified and expressed in a fibrant double category (proarrow equipment) which is biclosed.

Christian Williams (Apr 15 2021 at 04:01):

I have a strong feeling that there's a type theory for (multivariable) equipments in which co/ends are a more general and fluid notion of indexed sum and product.

Christian Williams (Apr 15 2021 at 04:04):

That's a different story. I just want to ask: how is coYoneda an expansion and how is Yoneda a reduction?

Christian Williams (Apr 15 2021 at 04:11):

actually, maybe a more universal terminology than $\eta$/$\beta$ would be co/evaluation.

Christian Williams (Apr 15 2021 at 04:14):

because we're talking about a generalized tensor-hom adjunction: $C(a\otimes b, c)\simeq C(a,[b,c])$ gives a unit "coevaluation" $\eta_{ab}: a\to [b,a\otimes b]$ and a counit "evaluation" $\beta_{bc}:[b,c]\otimes b\to c$.

Christian Williams (Apr 15 2021 at 04:17):

coevaluation, colimit, left adjoint, left extension, coYoneda, indexed sum, existential
evaluation, limit, right adjoint, right extension, Yoneda, indexed product, universal

Christian Williams (Apr 15 2021 at 04:18):

to clarify how extensions generalize the tensor-hom adjunction, we understand a bicategory as a multisorted monoidal category -- tensor becomes composition.

Christian Williams (Apr 15 2021 at 04:20):

Then we can ask if there is a right adjoint to precomposition: $K(f\circ i, g) \simeq K(f, [i,g])$

Christian Williams (Apr 15 2021 at 04:21):

So if it exists, this generalized hom $[i,g]$ is $Ran_i(g)$

Christian Williams (Apr 15 2021 at 04:24):

If we also have a right adjoint to the other tensor, postcomposition: $K(f\circ i, g)\simeq K(i, f\multimap g)$ that is right lifting.

Christian Williams (Apr 15 2021 at 04:26):

so, the multisorted form of a (bi)closed monoidal category is a bicategory with right extensions and liftings.

Christian Williams (Apr 15 2021 at 04:27):

that's great, but what about the left adjoints? I've been motivating a duality between left and right extensions.

Christian Williams (Apr 15 2021 at 04:30):

this is the part where I think if we use the dao of equipments there's a clear direction.

Christian Williams (Apr 15 2021 at 04:31):

any way this is a thread about co/yoneda as co/evaluation, both formally and philosophically.

Mike Shulman (Apr 15 2021 at 13:27):

The end that appears in coYoneda is a special case of composition in the bicategory of profunctors, and the end that appears in Yoneda is the corresponding special case of its right adjoint. Is that not what you're asking about?

Christian Williams (Apr 15 2021 at 15:34):

yes, it is

Mike Shulman (Apr 15 2021 at 15:38):

Ok, so what is the question exactly?

Christian Williams (Apr 15 2021 at 16:31):

just naively/philosophically, in what sense is coYoneda a coevaluation/$\eta$-expansion and Yoneda an evaluation/$\beta$-reduction?

Mike Shulman (Apr 15 2021 at 19:43):

Other than the sense in which one is the unit of an adjunction and the other is its counit?

Christian Williams (Apr 15 2021 at 22:57):

yes. and it's not just any adjunction, right? it's a tensor-hom adjunction.

Christian Williams (Apr 15 2021 at 22:59):

but yes I mean for example in proofs, do you find that you often use coYoneda as an "expansion" and Yoneda as a "reduction"? not always, but most of the time

Mike Shulman (Apr 16 2021 at 03:39):

I think I most often use them both as reductions.

Christian Williams (Apr 16 2021 at 20:16):

hm, okay. what's a good example of using coYoneda as a reduction?

Mike Shulman (Apr 16 2021 at 20:35):

Well, I just grepped through my own papers and the only occurrence of "co-Yoneda" I could find is on p14 of http://home.sandiego.edu/~shulman/papers/reedy.pdf.

Mike Shulman (Apr 16 2021 at 20:36):

But thinking about it a bit more I can see an "expansion" use of co-Yoneda in the form "any presheaf is a colimit of representables", which is less often called by the name "co-Yoneda" but is certainly a sort of expansion, starting with a presheaf and expanding it into a colimit.

Christian Williams (Apr 16 2021 at 20:37):

yes, that's how I was thinking

Christian Williams (Apr 16 2021 at 20:37):

people don't often use the term coYoneda, but they use this idea all the time.

Christian Williams (Apr 16 2021 at 21:44):

there's a funny asymmetry - coYoneda says "a presheaf is a colimit of representables" $A\simeq \int^c A(c)\times C(-,c)$, but Yoneda doesn't say "a presheaf is a limit of representables", because the representables are the arities: $A\simeq \int_c [C(-,c),A(c)]$