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: A pesky coequaliser

fosco (Sep 08 2020 at 12:43):

Let $\cal C$ be a category with $\sf Set$-tensors and enough colimits for the following to make sense.

The correspondence $(A,B,C)\mapsto {\cal C}[A,B]\otimes C$ is a functor ${\cal C}^\text{op}\times {\cal C} \times {\cal C} \to {\cal C}$; one can define a pair of parallel maps $\alpha,\beta$, in the diagram

$\displaystyle \coprod_{u : A\to B} {\cal C}[B,A]\otimes A \,\overset{\alpha}{\underset{\beta}\rightrightarrows} \coprod_{A\in\cal C} {\cal C}[A,A]\otimes A$

by the rules $\alpha(u; f,x)=(f u, x) \in {\cal C}[A,A]\otimes A$ and $\beta(u; f,x)=(uf, ux) \in {\cal C}[B,B]\otimes B$.

I'm trying to compute the coequaliser of the pair $\alpha,\beta$: it should be a quotient of $\coprod_{A\in\cal C} {\cal C}[A,A]\otimes A$ by a certain equivalence relation; in the form of a family of arrows

$\zeta_A : {\cal C}[A,A]\otimes A \to Z$

with the property that (using element notation a bit liberally, or if you want, let $\cal C=\sf Set$)

$\zeta_A(fu,x)=\zeta_B(uf,ux)$ for every $f : B\to A,u : A\to B, x\in A$

and initial with respect to this property. I'm unable to find even a candidate for this map. Any suggestion?

Morgan Rogers (he/him) (Sep 08 2020 at 13:26):

Should the index on the second coproduct be $A \in \mathcal{C}$ rather than $A \in \mathbf{Set}$?

fosco (Sep 08 2020 at 13:52):

whooops

Morgan Rogers (he/him) (Sep 08 2020 at 14:23):

I can't quite see how you would avoid problematic size issues in defining that coproduct. In $\mathbf{Set}$, for example, you're taking a coproduct indexed by the entirety of $\mathbf{Set}$, which will be Too Big. Do you have a reason to think that, even if that coproduct isn't well-defined, the coequalizer you're interested in should be?

fosco (Sep 08 2020 at 14:28):

What I'm interested into is an ansatz in a situation where size isn't a problem, and then I'll try to see whether (as you correctly pose it) even if that coproduct isn't well defined, the coequaliser exists.

fosco (Sep 08 2020 at 14:55):

I know it's not exactly polite to throw you a computation without context :grinning: I'm just short of good ideas to find this answer...

Morgan Rogers (he/him) (Sep 08 2020 at 15:21):

That's a relatable sentiment :grinning_face_with_smiling_eyes:

Dan Doel (Sep 08 2020 at 17:43):

This is probably no help, but it reminds me of the sort of property that would hold in type theory for something written like $\displaystyle \exists_{A \in C} C[A,A] \otimes A$, where $∃$ is a 'parametric' sum. That would lead one in category theory to ask about the coend $\int^{A \in C} C[A,A] \otimes A$, which seems like it would have this sort of property (extranaturality).

But I guess that doesn't answer whether the coend exists, which is what is actually desired?

fosco (Sep 08 2020 at 17:48):

Dan Doel said:

This is probably no help, but it reminds me of the sort of property that would hold in type theory for something written like $\displaystyle \exists_{A \in C} C[A,A] \otimes A$, where $∃$ is a 'parametric' sum. That would lead one in category theory to ask about the coend $\int^{A \in C} C[A,A] \otimes A$, which seems like it would have this sort of property (extranaturality).

But I guess that doesn't answer whether the coend exists, which is what is actually desired?

On the contrary, the question is actually "what is the coend of $C[A,A]\otimes A$?

Dan Doel (Sep 08 2020 at 17:59):

Well, I don't know in general. For types/sets it seems like it would be the terminal object.

Dan Doel (Sep 08 2020 at 18:08):

I guess for more reasoning on how I got there, it looks like an encoding of the final coalgebra for the identity functor. There is a 'hidden' type $A$, a current state with type $A$, and a way of stepping to the next state. But there are no observations to make, so all states are equivalent.

fosco (Sep 08 2020 at 19:01):

Had the same gut feeling, but I couldn't prove directly that every cowedge for $[A,A]\times A$ is constant. If it's true, it surely is implied by the fact that a cowedge $\zeta$ must satisfy $\zeta_A(fu,x)=\zeta_B(uf,ux)$.

@Théo (<- I'm taggin in this conversation the person for which this is relevant :-) )