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: learning: questions

Topic: what kind of dual is coYoneda?

Jade Master (Oct 10 2022 at 21:33):

What exactly is being dualized to obtain the coYoneda lemma from the Yoneda lemma. Is it just that coYoneda has a coend and Yoneda has an end?

Reid Barton (Oct 10 2022 at 22:31):

Do you have a specific "coYoneda lemma" statement in mind?

Christian Williams (Oct 10 2022 at 23:07):

Composition of profunctors is "tensor": given $P:A\to X$ and $Q:X\to B$,
$(P\otimes Q)(a,b)$ is $(\sum x.\; P(a,x)\times Q(x,b))$
quotiented by $(x_0,(p,x\cdot q))\sim (x_1,(p\cdot x,q))$ for all $x:x_0\to x_1$ in $X$.

Thinking of profunctor elements as heteromorphisms, this quotient is "associativity across $X$"; but it's also what makes profunctor composition unital, $(A\otimes P)\simeq P$:

$\int a_1:A.\; A(a_0,a_1)\times P(a_1,x)\simeq P(a_0,x)$.

The forward direction is left action $(a:A(a_0,a_1),p:P(a_1,x))\mapsto (a\cdot p):P(a_0,x)$, and the inverse is inserting the left unit: $(p:P(a_0,x))\mapsto (1_{a_0},p)$. This is an iso because of the quotient: any $(a,p)$ gets sent to $(1_{a_0},a\cdot p)$ which in the quotient is equal to $(a,p)$.

This is coYoneda: every profunctor has a canonical "colimit expansion" on either side, given by unitality of composition.

Max New (Oct 10 2022 at 23:09):

In double-category/profunctor terms, the Co-Yoneda lemma says that tensoring (profunctor composition) with the unit (hom set) is the identity and the Yoneda lemma says that powering (profunctor hom) with the unit is the identity. I.e., Co-Yoneda is analogous to $I \otimes A \cong A$ and Yoneda is analogous to $I \multimap A \cong A$ in monoidal closed categories.

Christian Williams (Oct 10 2022 at 23:13):

Dually, transformation of profunctors is "hom": given $R:A\to B$ and $S:A\to B$, the set of natural transformations $[R,S]$ is the subset of $\prod ab.\; R(a,b)\to S(a,b)$ which satisfy naturality

$\gamma(a_1,b_1)(a\cdot r\cdot b) = a\cdot \gamma(a_0,b_0)(r)\cdot b$
for all $(a:a_0\to a_1,b:b_0\to b_1)$.

This hom is an equalizer of a product, "dual" to the tensor above, a coequalizer of a sum. But note that the tensor is over a middle variable, while the hom is over both outer variables. The "duality" is not that one becomes the other by "(-)^op"; it is rather a two-dimensional version of tensor and hom.

Christian Williams (Oct 10 2022 at 23:17):

So I'd say "the real duality" is between this tensor and hom.

We just care a lot about its (important) application to categories' identities, which are homs: coYoneda is unitality of composition, and Yoneda is currying this on either side.

Christian Williams (Oct 10 2022 at 23:24):

Much has been written online as to how Yoneda means that "an object can be known through its connection to everything else." I think it can be said concisely by the fact a category's very identity is its hom.

I think of this as "concrete, flowing identity-through-difference" as opposed to "abstract, static equality".

Christian Williams (Oct 11 2022 at 00:31):

This is all worth fleshing out more and drawing pictures, which would be fun to do here. I was just giving a summary.

Jade Master (Oct 11 2022 at 09:20):

In what sense is the composition in Prof a tensor? Usually a tensor-hom adjunction involves a monoidal category but what we're talking about is the composition operation? What is a tensor-hom adjunction in this context?

Jade Master (Oct 11 2022 at 09:26):

Ohhh wait...restricted to a category C, Prof becomes a one object bicategory...and even better it's monoidal closed...with the adjunction passing between Yoneda and coYoneda for the monoidal unit :)

fosco (Oct 11 2022 at 09:36):

Jade Master said:

What exactly is being dualized to obtain the coYoneda lemma from the Yoneda lemma. Is it just that coYoneda has a coend and Yoneda has an end?

If you don't want to see it through profunctors, here's another way to look at this story: "the Yoneda embedding" is in fact two functors:, obtained as the two mates of $\hom : C^{op}\times C \to Set$ under the Cartesian closed structure of Cat:

• the covariant Yoneda embedding is $y : C \to [C^{op},Set]$
• the contravariant Yoneda embedding is $y' : C\to [C,Set]^{op}$

now if you call $PC=[C^{op},Set]$ and $P'C=[C,Set]^{op}$, you see that $PC = P'(C^{op})^{op}$, and for the same reason $P'C=P(C^{op})^{op}$. So, the Yoneda lemma that involves a statement about $PC$ can be rephrased into a statement that involves $P'(C^{op})^{op}$ and vice versa

Jade Master (Oct 11 2022 at 10:17):

Jade Master said:

Ohhh wait...restricted to a category C, Prof becomes a one object bicategory...and even better it's monoidal closed...with the adjunction passing between Yoneda and coYoneda for the monoidal unit :)

Actually I'm not sure if this is true

Max New (Oct 11 2022 at 11:17):

The adjunction is described in Benabou's notes: http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf

Max New (Oct 11 2022 at 15:30):

Nlab has a stub about this generalization of tensor/hom: https://ncatlab.org/nlab/show/closed+bicategory

Christian Williams (Oct 11 2022 at 18:10):

Jade Master said:

In what sense is the composition in Prof a tensor? Usually a tensor-hom adjunction involves a monoidal category but what we're talking about is the composition operation? What is a tensor-hom adjunction in this context?

Like Max said, a closed bicategory is a horizontal categorification of a closed monoidal category. We have the adjunctions $\mathrm{Prof}(P\circ Q, R) \simeq \mathrm{Prof}(P, R / Q)$ for right lifts, and $\mathrm{Prof}(P\circ Q, R) \simeq \mathrm{Prof}(Q, P \backslash R)$ for right extensions.

It deserves to be called a tensor because composition of V-profunctors generalizes the tensor of ordinary modules; the quotient ensures "linearity" (naturality) in its middle variable when one maps out of the composite and considers these adjoint equivalences above.

Jade Master (Oct 12 2022 at 13:29):

@fosco when you phrase the Yoneda in P'(C^op)^op do you get the fact about every presheaf being a colimit of representables or is it something else?