Just did my first actual computation with coends and I can FEEL the power flowing through me.
@hallasurvivor tfw you've reached the final level of category theory
Ooooh, if there's one thing I'm intimately aware of, it's that there's always more levels to category theory, haha.
@hallasurvivor that's always true, but also, what levels are there beyond coends? :D unless maybe 2-coends of some kind
@Zanzi *dead eyes, thin hollow voice* Oh, there are levels beyond coends.
@nilesjohnson @hallasurvivor do tell me more. i am intrigued yet horrified, as perhaps these levels are so deep that no human could delve so far and remain sane
@Zanzi Ha ha ha! I was mostly just thinking of how confusing the different variants in dimension 2 can be (universal property up to isomorphism, or equivalence, or something even weaker).
But now you've made me wonder about the relationship between lax (co)ends and general weighted (co)limits for some specific weight. I don't know (can't remember) exactly whether all weighted (co)limits can be computed as (co)ends. Furthermore, I think that usually Kan extensions can be computed as certain ends, but the two concepts don't always coincide (especially for enriched categories, where I think the notion of Kan extension is not so clear).
But I am *not* going to get nerd-sniped right now! :) Maybe someone else here can be more definitive.
And of course, the more important thing is to celebrate each bit of progress someone makes into that dark forest :)
@nilesjohnson @Zanzi @hallasurvivor All weighted colimit can be computed as coends, indeed. This screenshot is from the Coend calculus book.
Not sure about the lax version though
@bgavran @nilesjohnson @Zanzi @hallasurvivor W should be contravariant here, right? (Both to serve as a weight for a colimit, and to make the coend given there non-mute)
@ayegill @nilesjohnson @Zanzi @hallasurvivor
Ah, yes. This was confusing me for a while when I first saw it.
On a shallow level I understand that coend formulation of weighted colimits uses copowers (which are covariant in both variables) and that end formulation uses powers (which are contravariant in one variable).
This then means that contravariance (as necessitated by the coend) has to go somewhere, and it goes in the weight.
But outside of the coend formulaton I don't intuitively understand why colimits would need contravariant weights.
@bgavran @nilesjohnson @Zanzi @hallasurvivor The simple explanation is that "colimits are just limits in the opposite category". If I have a diagram X: I --> C and want to compute a limit in C^op, the dual is a diagram I^op --> C^op. So to compute a weighted limit of this, I need a weight on I^op, not on I.
@ayegill @bgavran @nilesjohnson @hallasurvivor this is the part of CT that I've always struggled with. I think I'll need to see some code to make sense of it personally!
@ayegill @nilesjohnson @Zanzi @hallasurvivor
Right, that makes perfect sense. I was so deep in the coend world that I forgot about this simple fact
@bgavran @nilesjohnson @Zanzi @hallasurvivor More concretely, the role that W(i) plays in a weighted limit is as an index object for the maps into X(i) - instead of asking for one map from the limit into each X(i), I ask for W(i)-many maps (meaning, a map W(i) --> [A, X(i)]. The functoriality of W tells me how these maps are supposed to be related under postcomposition by the maps in the diagram.
Then if I'm doing a colimit, this is *precomposition*, so the functoriality goes the other way.