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: ends and limits

Jacques Carette (Aug 17 2020 at 02:45):

I am slowly trying to learn about co/ends by systematically formalizing Loregian's textbook https://arxiv.org/pdf/1501.02503.pdf. It's been somewhat of a struggle - the first ½ of p.13 alone has taken me 3 days, just to unpack everything that's there! And I am now stuck on the lhs of Eq. (25) of p.13. I do have a proof that Limits are terminal Cones, Ends are terminal Wedges, categorical equivalences preserve terminal objects (that was monstrously hard too). So I have the two arrows that witness that the two objects are equivalent, what I'm stuck on is that they are inverses.

This is surely where the comment about terminal objects being preserved comes in (as I have not used that result yet), but I'm still stuck.

Simon Burton (Aug 17 2020 at 15:02):

What language are you using for the formalization?

Jacques Carette (Aug 17 2020 at 15:16):

Agda. It's intended to go into agda-categories.

Morgan Rogers (he/him) (Aug 18 2020 at 07:12):

My advice would be to stick as close as possible to the standard "uniqueness up to isom of universal constructions" argument. In this case, it would go something like observing that the arrows between the end and limit commute with the arrows defining the end wedge and the limit cone in a suitable way, so that when you compose both of them with the limit cone, say, the result is the same limit cone, which forces that composite to be the identity.

Morgan Rogers (he/him) (Aug 18 2020 at 07:12):

If that was too vague, I can sketch some diagrams :joy:

fosco (Aug 18 2020 at 07:43):

I doubt I can help you with the agda code, but I disassembled and reassembled those proofs inside out 25 times already. Maybe among all possible proofs I can help you find the simplest one to formalise.

Jacques Carette (Aug 18 2020 at 13:04):

Turns out that if I interpret $\cong$ in Eq. (25) to be in the category Wedge F instead of in $D$ (where $F : C^{\text{op}} \times C \rightarrow D$), the result indeed follows by the fact that the just-proved categories are equivalent, and equivalence preserves terminal objects. As a second step, this induces the result on objects of D. The two proofs are then completely straightforward.

What was really not clear to me was that I needed to first to the proof in Wedge F, to get the result in D as a corollary.

Jacques Carette (Aug 18 2020 at 13:07):

@fosco I would greatly appreciate the help! I can handle the Agda side of things. Do you prefer that we continue to exchange messages here, or do you prefer a different medium of communication?

fosco (Aug 18 2020 at 13:08):

Let's keep it public for the moment! I know a few people proficient in Agda, probably they can help too

Jacques Carette (Aug 18 2020 at 13:09):

Glad to. I'll keep posting here (and in this stream, but using new topics as appropriate).

Jacques Carette (Aug 18 2020 at 13:14):

So, if you're keeping notes for a 2nd edition of your book, on top of the above confusion of how to prove that particular remark: 'equivalence of categories preserves initial and terminal objects' is true, but requires 'adjoint equivalence' as far as I can tell. Of course, all equivalences can be so upgraded, but it took me forever to see that the 'obvious' arrow was simply not going to work in the uniqueness proof, but that 'zig' would.

Reid Barton (Aug 18 2020 at 14:59):

I'm not sure what your setup is, but the proof should just be: if $F : C \to D$ is an equivalence and $X$ is a terminal object of $C$, then we want to prove $FX$ is a terminal object of $D$: Let $B$ be an object of $D$; we want to show $D(B, FX)$ has a single element; pick an object $A$ and an isomorphism $FA \cong B$ (we can do this because $F$ is an equivalence); then $D(B, FX) \cong D(FA, FX) \cong C(A, X) \cong *$.

Eric Schles (Mar 31 2022 at 14:26):

:wave: I have a question about Ends & CoEnds - I'm trying to come up with some examples for Ends & CoEnds in specific categories. Is it correct to say the general procedure for coming up with an End is:

Algorithm for Ends:

1. Come up with two functors on C - one that is covariant and another that is contravariant. Verify that they are functors.
2. guess a profunctor on C[op] x C -> Set (for a Category, C), from the functors in step 1. Then check that it is indeed a profunctor.
3. specify a projection map for profunctor, identity map for the category.
4. Come up with your wedge condition.
5. Check the wedge condition using your profunctor, your projection map, and your identity map. Aka check the naturality condition.

in otherwords Forall a: fa -> gb such that the naturality condition holds.

Does this seem right/ reasonable?

fosco (Mar 31 2022 at 21:12):

A coend is a certain universal object attached to a functor of type $C^{op}\times C \to D$; a way to produce such a functor is to take a covariant $F : C \to D$, a contravariant $G: C^{op}\to D$, a "product" $*:D\times D \to D$, and consider the functor $(c,c')\mapsto Gc * Fc'$.

Dually, for an end, you might want to consider two functors $F,G : C\to D$ of the same variance, and then a functor $[-,-] : D^{op}\times D \to D$, and then the functor $(c,c')\mapsto [Fc, Gc']$.

But this is not the only way to obtain such objects! There's plenty of functors that are not "decomposable" into $F*G$ as above.

fosco (Mar 31 2022 at 21:14):

If the domain of $F,G$ is small and their codomain is $Set$, the end of $F*G$ always exist; it might be far from interesting, but you can compute it.

Eric Schles (Apr 01 2022 at 11:24):

Thanks!

Eric Schles (Apr 01 2022 at 11:27):

A somewhat more trivial question - I'm pretty sure the CoEnd for Vect is the tensor product defined here: https://en.wikipedia.org/wiki/Tensor_product (got to Tensor product of linear maps). I _think_ the End would be Span for Vect? Does that seem right? It feels weird that Span would be dual to Tensor Product though in some sense. So just want to check my logic.

John Baez (Apr 01 2022 at 14:51):

I don't think coends in Vect are the usual tensor products in Vect. That sounds too exciting to be true. Tensor products "know about" bilinear maps while Vect, as a mere category rather than a monoidal category or multicategory, only "knows about" linear maps.

John Baez (Apr 01 2022 at 14:52):

But maybe I'm missing the point here.

fosco (Apr 01 2022 at 19:42):

What you claim is not exact, but the tensor product of vector spaces (or R-modules, for that matter) can be characterised as a coend, yes. A left R-module is a functor $R\to Ab$, regarding the monoid $(R,\cdot)$ as a category with a single object (in fact, an $Ab$-enriched category with a single object!); dually, a right R-module is a functor $R^{op}\to Ab$. The "functor tensor product" of the two is their tensor product as modules (or more precisely, its underlying abelian group)

fosco (Apr 01 2022 at 19:44):

Slightly more conceptually, you can define a bicategory $Mod$ whose 0-cells are rings (all unital rings), and where the hom-category $Mod(R,S)$ is the category ${}_R Mod_S$ of left-$R$, right $S$-bimodules.

In this perspective, given modules $M : R \to S$ and $N : S\to T$, their composition as 1-cells is the $R,T$-bimodule $M\otimes_S N$.

fosco (Apr 01 2022 at 19:50):

In both cases the claim is easy to motivate because the coequaliser that defines the tensor product (modding out the abelian group $M\otimes N$ by $R$-bilinearity) is precisely the coequaliser yielding the coend that defines the functor tensor product, identifying $M,N$ as functors.

In the second picture, $Mod$ "is" a bicategory of profunctors, and in fact can be identified with the subcategory of $Ab$-enriched profunctors between "1-object $Ab$-enriched categories", i.e. unital rings. Profunctor composition is defined by a coend, the same coend that defines the aforementioned (functor) tensor product.

Jan Pax (Apr 02 2022 at 16:39):

I have a very trivial question about the page 80 here: how this shape of $W$ $W:2\to \mathbf{Set}$ with $\ast\sqcup\ast\to \ast$ implies that the components of $W\Rightarrow\cal{M}(m,f)$
are these two arrows $h:m\to a,k:m\to a,$
and that that diagram should commute.
Perhaps that I've entirely forgotten what a natural transformation is for this case! I understand that the arrows should be 2 in number, though. I do not understand the direction of $h,k$ as from $m\to a$. 4.jpg

fosco (Apr 03 2022 at 13:44):

A natural transformation $W \Rightarrow \hom(m,F)$ has two components:

• $W0 \to \hom(m, F0)$ picks two elements from $\hom(m, F0) = \hom(m,a)$; call them $h,k$
• $W1 \to \hom(m, F1)$ picks an element from $\hom(n, F1)=\hom(m,b)$; call this element $u$

now, naturality at $0\to 1$ yields a commutative square (draw it!) and imposes the condition that $fh=fk=u$.

Jan Pax (Apr 03 2022 at 14:18):

Why $W0 \to \hom(m, F0)$ picks two elements from $\hom(m, F0) = \hom(m,a)$,
while $W1 \to \hom(m, F1)$ picks single element ? Thank you.

fosco (Apr 03 2022 at 17:34):

well, $W0$ is a two element set, $W1$ is a singleton...

Jan Pax (Apr 03 2022 at 17:43):

Please be patient with me, how do you know that $W0$ is a 2 element set from what is given on that page 80 ?

Reid Barton (Apr 03 2022 at 17:52):

Isn't that the definition of $W$? Or what do you think the definition of $W$ is?

Jan Pax (Apr 03 2022 at 20:50):

(deleted)