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: Terminology: natural element of a profunctor

Max New (Jul 23 2024 at 13:35):

I've encountered the following concept in working with formal category
theory and mechanized category theory in Agda and I wonder if there's
an existing name for it because I haven't found one:

A profunctor homomorphism (i.e., a natural transformation) $\phi$
from $\textrm{Hom} : C^{op} \times C \to \textrm{Set}$ to any $R : C^{op} \times C \to \textrm{Set}$ is
determined by where it sends the identity morphisms. In fact any
choice of where to send the identity morphisms extends to a profunctor
homomorphism as long as it satisfies a "naturality" condition.

Define a natural element $\alpha$ of a (endo-)profunctor $R : C^{op} \times C \to \textrm{Set}$ to be

1. A family of elements $\alpha_x : R(x,x)$ for every $x$
2. Such that for every $f : C(x,y)$, $R(x,f)(\alpha_x) = R(f,y)(\alpha_y)$

A couple examples of where this comes up:

1. This gives a universal property for Hom in the category of endo-profunctors: $\textrm{id}$ is the universal natural element.
2. This is a natural definition of the "nullary" 2-cells in the virtual equipment of categories,functors,profunctors,and homomorphisms
3. Natural transformations $F \Rightarrow G : C \to D$ can be defined as natural elements of $D(F-,G=)$.

I'm sure others have encountered this concept so I wonder if there's an existing name for it?

Todd Trimble (Jul 23 2024 at 14:05):

This is the end $\int_x R(x, x)$, and I think maybe I have seen a name for it or something similar to it. There's a dual form $\int^x R(x, x)$ which is called the trace of the endofunctor.

Todd Trimble (Jul 23 2024 at 14:07):

Ah, it's called the center.

Max New (Jul 23 2024 at 18:19):

to be clear: the center there means the end $\int_x \textrm{Hom}(x,x)$ specifically right? Not for an arbitrary $R$?

Todd Trimble (Jul 23 2024 at 19:26):

I guess that's right. I'm not sure I can find off-hand another reference that gives the center of an endoprofunctor, but @Tom Leinster might know. (I have some vague memory this could have come up in connection either with the eventual image, or his papers on Julia sets as terminal coalgebras.)

The trace of an endoprofunctor on the other hand is very well motivated terminology. Just as the classical trace of an endomorphism on a finite-dimensional vector space can be defined in terms of the compact closed structure on $\mathsf{Vect}_{fd}$, so the trace of an endoprofunctor can be described the same way, using the compact closed structure on the bicategory of small categories and profunctors between them.

Nathanael Arkor (Jul 23 2024 at 20:13):

The end $\int_x R(x, x)$ is called the cotrace of $R$ in @Callum Reader's thesis Scalar enrichment and cotraces in bicategories, e.g. see Example 6.5.11.

Todd Trimble (Jul 23 2024 at 20:19):

Oh, good. Day and Street use this terminology as well.

Max New (Jul 23 2024 at 20:58):

and I guess they don't have a name for the elements of the cotrace as they are working with enriched profunctors