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: community: our work

Topic: fosco

fosco (Dec 08 2023 at 14:06):

It's the first time I post here. I am happy to get some feedback for a paper that I have been working for quite a bit, together with @Greta Coraglia , @Ülo Reimaa , (or @Ülo Reimaa ?) and Davide Castelnovo.

The paper is "The fibration of algebras", it's temporarily hosted on my page, here, and for some time we felt its subtitle might have been something like "feels like a bunch of things that should have been observed somewhere, but weren't, so here we are with an 80-ish pages long note"

The paper in a nutshell: often one is led to study functors that "depend on one or more parameters". For example: there is a polynomial endofunctor sending a set $S$ to $1 + A \times S$, one functor for every set $A$. This is a nice polynomial, that people studied a lot (especially its algebras: the initial object in its category of algebras is $List(A)$). But now, instead of the functor $F_A = 1 + A \times (\_)$, in order to classify "the polynomial", it would be very convenient to study its shape, i.e. the "anonymous" functor $\lambda A.F_A : Set \to [Set,Set]$ sending a given parameter to the functor taken at that particular parameter. This association is itself a functor, and now one can say: to understand the polynomial, let's study its category of algebras, but with respect to all parameters at the same time, or rather, coherently taking into account the various parameters.

This begs various questions: 1) how does one collect all the various categories Alg(F_A) together? 2) What is a similar construction for a more general polynomial, or a more general parametric functor? 3) Are there other examples? 4) Does this theory scale easily (for example: what if $F_A$ is a co/monad, are there other examples in this sense)?

The paper gives various answers: 1) You build a fibration, the "fibration of algebras" of the title, over a category $A$ of parameters, for a family $F_A : X\to X$ of endofunctors. 2)-3) There are enough examples to work on this for a couple of years, which I plan to do. 4) The theory scales extremely well: for example, a parametric monad $T : A \to [X,X]$ is just a monad in a certain coKleisli category; and its fibration collecting all the Eilenberg-Moore (resp. Kleisli) $EM(T_A)$ is its EM-category (resp., $Kl(T_A)$ is a Kleisli category).

fosco (Dec 08 2023 at 14:09):

It turns out, and this was totally unexpected when we started studying this stuff, that a fruitful way to think of all the EM(T_A) stitched together is as a semidirect product (hence all my questions on the matter, here, lately) $A ⋉ X$, where $T$ abstracts a way the monoidoid $A$ acts via homomorphisms on another monoidoid $X$. (Currying the parametric monad $T$ into a functor $A\times X \to X$ is an action of $A$ on $X$, after all!)

This is exciting for a variety of reasons:

1) sending (A,X,T) to $A⋉X$ is a functor from a domain of the form $Cat ⋉ Cat$, shoutout to the [[microcosm principle]]!

2) the operations of semidirect product of groups is a left adjoint to a canonical functor $Grp \to Grp ⋉ Grp$

3) the categories $A,X$ fit into a short exact seq. $1 \to X \to A⋉X \to A \to 1$, which is universal in a 2-category of "extensions of A by X" $Ext^1(A,X)$ (yes, we have an analogue of Baer sum: Ext¹(A,X) is symmetric monoidal as soon as $A,X$ are pointed categories).

4) Examples of this construction are: the simple fibration in categorical logic, the category of cocommutative Hopf algebras on a field of characteristic zero, thanks to the celebrated Cartier-Gabriel-Kostant "reconstruction" theorem, Beck modules, and many, many, many, many, others.

fosco (Dec 08 2023 at 14:16):

The paper is very quirky in many ways: it's very long. It strives for the maximal level of generality in some respects, as much as we could provide, but some of its ideas feel like a hack (we don't know why some results are trivially trivial, so to speak). Proofs are omitted. It ends abruptly, just before we have some leverage to really apply this language somewhere; but most importantly, it ends by acknowledging how uncommon it is that we acknowledge how difficult it was to write down something that in hindsight is "totally obvious".

I really care about this stuff, I have been thinking about it on-and-off since March 2022; yet, I still feel these many pages have just scratched the surface of a longer, deeper story, that probably can be told better than I did, with immense help from my coauthors.

I will happily listen to your feedback.

Matteo Capucci (he/him) (Dec 11 2023 at 08:42):

Very interesting fosco. My attention was captured by an example I missed before, the simple fibration. Recently I realized I need to talk about it in general complete 2-categories, but I couldn't come up with an abstract definition.
It seems like you did!
Correct me if I'm wrong, but you show that, in $\bf Cat$, the simple fibration $S(\cal X) \to X$ associated to a cartesian category $\cal X$ is the co-Kleisli fibration of the monad $\times : \cal X \times X \to X$ in $\bf Fib(\cal X)$. Am I wrong? And do you expect this result to generalize to suitable 2-categories?

fosco (Dec 11 2023 at 13:34):

I will use a slightly different notation than in the paper, but yes, this is somehing we cover there.

What we call the "regular representation" of a Cartesian category is the parametric functor arising from the product: for each fixed $A$ in $Cat$ you then get a comonad $A\times -$. The regular representation exists, of course, for every monoidal category, but $A\otimes -$ is a comonad only for the Cartesian structure.

If your category is in fact a 2-category, now, you can consider all the following objects:

• the endofunctor algebras for $A\times -$ regarded as endofunctor
• the coEilenberg-Moore algebras taking into account the comonad structure
• the cofree coalgebras, so the coKleisli category of $A\times-$

and in each of these two cases you can consider strict algebras, pseudoalgebras, lax algebras, oplax algebras... and each case gives rise to a fibration or opfibration.

fosco (Dec 11 2023 at 13:37):

Now an endofunctor algebra for $A\times-$ is a functor $A\times X \to X$ for some $X$, i.e. an endo-1-cell $X\to X$ in the coKleisli category of $A\times-$, so a parametric endofunctor is an endo-1-cell in $coKl(A\times-)$, and a parametric monad is a monad in $coKl(A\times-)$, and a comonad is a monad in in $coKl(A\times-)$, all over the object $X$.

fosco (Dec 11 2023 at 13:45):

In a generic 2-category I would say that you can define some flavour or the fibration of coKleisli categories of $A\times-$ (according to whether you need strict algebras, pseudo, lax, oplax...) and "the simple fibration" is the fibration that you get from a "Cartesian object" as... ah, I have to write more than I can now. But yes, I think I can obtain what you want, although it will be somewhat tautological.

The non-tautological step is that some universal construction made of inserters and equifiers gives a fibration (in general, $Ins(f,g) \to X$ is not a fibration for two parallel $f,g$).

fosco (Dec 11 2023 at 13:52):

A Cartesian object of $\mathcal K$ (ambient Cartesian 2-category) is a 0-cell such that $A\to A\times A$ is a left adjoint. The right adjoint is "product structure".

Every Cartesian object of $\mathcal K$ induces a regular representation $A\times A \to A$ through its product structure, and thus a parametric endo-1-cell starting the machinery of §4.7.1.

Matteo Capucci (he/him) (Dec 11 2023 at 14:05):

It seems the answer is yes. But I'm lost in the details.
Here's my guess:

You start with a parametric comonad $A \times A \to A$, arising from the 'regular representation' of a cartesian object $A$ in a 2-category $\cal K$. Now this is a comonad over $\pi_1:A \times A \to A$ in ${\cal K}/A$. Take coKleisli object. This is the simple fibration associated to the cartesian object $A$.

fosco (Dec 11 2023 at 14:14):

Yes, I think if K=Cat and the comonad is "product by an object" this is exactly what you get. Fix a category $A$, "product by an object" is a parametric comonad $S : A \not\to A$ in $coKl(A\times-)$, i.e. each $S_a : A\to A$ is a comonad and naturally so.

The coKleisli object of this comonad in the sense of the formal theory of comonads in a certain 2-category is the simple fibration that Jacobs defines.

fosco (Dec 11 2023 at 14:16):

Should I write this more explicitly? Probably it deserves to be remarked.
Also: I think in a generic 2-category there's nothing more, nothing less than this, you only lose the possibility to "evaluate" $S$ on points of $A$

Matteo Capucci (he/him) (Dec 11 2023 at 16:00):

Indeed!

Matteo Capucci (he/him) (Dec 11 2023 at 16:03):

Maybe you wrote this explicitly enough for the general case, I was just too lazy to do my homework :grinning_face_with_smiling_eyes: there doesn't seem to be a specific example for the simple fibration, no

fosco (Dec 12 2023 at 11:27):

I added a few lines that clarify this point.
image.png

Crossrefs might have changed, but at the same link there is an updated pdf! As of today, Remark 4.2.8 covers what I told you yesterday. It was implicitly stated, but it's better this way.

Matteo Capucci (he/him) (Dec 12 2023 at 11:53):

Lovely! I now realize @Jules Hedges told me something like this a long time ago.

fosco (Dec 12 2023 at 11:53):

in what context? This exact statement? :grinning:

Matteo Capucci (he/him) (Dec 12 2023 at 11:57):

More or less. I'm having a hard time recalling... I just remember it was an observation about lenses: the simple fibration is the opposite fibration of 'simple' lenses, while the arrow fibration is the opposite of dependent lenses. Jules told me something like, the first is a coKleisli construction and the second a coEM, but this doesn't check out so I must misremember something

Matteo Capucci (he/him) (Dec 12 2023 at 11:57):

Let's see if he chips in

Matteo Capucci (he/him) (Dec 12 2023 at 11:57):

In general, I guess you are aware that in optics & related topics we do have a fair share of parametric endofunctors, like actegories

fosco (Dec 12 2023 at 11:58):

ah, I remember something like that on twitter (lol), where I was telling him "hmm, this looks like the simple fibration"

fosco (Dec 12 2023 at 11:58):

Matteo Capucci (he/him) said:

In general, I guess you are aware that in optics & related topics we do have a fair share of parametric endofunctors, like actegories

yep, part of this was also motivated by actegories

Jules Hedges (Dec 13 2023 at 17:29):

Here's the full thing:
If your category has finite products:

• Simple fibration: $\int \mathrm{coKl} (X \times -)$
• Lenses: $\int \mathrm{coKl} (X \times -)^\mathrm{op}$

If your category has finite limits:

• Arrow category: $\int \mathrm{coEM} (X \times -)$
• Containers (or polynomial functors if your category is also LCCC): $\int \mathrm{coEM} (X \times -)^\mathrm{op}$

Jules Hedges (Dec 13 2023 at 17:29):

Using the neat fact that $\mathrm{coEM} (X \times -) \cong \mathcal C / X$

Jules Hedges (Dec 13 2023 at 17:32):

All of these are written in different places (only the one for lenses came from me)

fosco (Dec 13 2023 at 18:00):

Nice. Do you have it written down somewhere, so I can cite it?

fosco (Dec 14 2023 at 09:08):

Also, can you clarify your notation when you say $\int C_x^{op}$, what do you mean exactly? The opposite fibration, the opposite of the total category, the fiberwise opposite...?

Jules Hedges (Dec 14 2023 at 12:05):

fosco said:

Nice. Do you have it written down somewhere, so I can cite it?

Afraid not. I ought to record it in a blog post, but the best I can do is trying to remember where they're all individually recorded. The simple fibration is in Bart's book, lenses is in my paper "Morphisms of open games", for the arrow category I think I found it in Handbook of Categorical Algebra, and for containers it's probably in the original Containers paper ("Categories of Containers" by Abbott et al) or in Abbott's PhD thesis

Jules Hedges (Dec 14 2023 at 12:06):

fosco said:

Also, can you clarify your notation when you say $\int C_x^{op}$, what do you mean exactly? The opposite fibration, the opposite of the total category, the fiberwise opposite...?

By this I mean the fibrewise opposite of the total category, ie. apply the Grothendieck construction to $F : \mathcal C^\mathrm{op} \to \mathbf{Cat}$, $F (X) = \mathrm{coKl} (X \times -)^\mathrm{op}$ etc

Nicolas Blanco (Dec 20 2023 at 15:00):

Nice, I was waiting for this paper since I saw your talk (at ItaCa iirc). Now I need to find some time to read it :) So I'm not sure how much of this comment will be relevant to your work.
What you presented made me think of some work I did during my PhD and that ended up in my thesis. I've been meaning to write a paper about it but haven't had the time. Some context: like you mentioned in the paper, the Grothendieck construction can be understood as a strict 2-pullback of categories and pseudofunctors. But this picture cannot directly be extended to, for example, the Bénabou-Grothendieck correspondence between functors and lax normal functors into Dist, the bicategory of distributors (or profunctors). Basically it is because of the laxity of the functors: you cannot define the composition in the pullback pairwise, since two images along the lax functors won't agree. The idea to get around this is to take composition not as a data but defined it universally with virtual double categories and then to use op-fibrations of vdcs to lift the composition from the domain of the lax functor to the Grothendieck construction. It's also interesting conceptually since it gets a fibrational perspective on the Grothendieck construction.

Nicolas Blanco (Dec 20 2023 at 15:00):

Going a bit more into the details: in a vdc, there are "universal cells" whose codomain is the composition of horizontal maps. Then given a functor of vdcs, one can define a notion of "opcartesian cell" which is a cell in the domain vdc that has a similar universal property than a universal cell but parametrised by a cell in the codomain. This is really a categorification of opcartesian multimaps for opfibrations of multicategories. Now, it is not hard to prove that an opcartesian cell over a universal cell is universal. That means that given a functor of vdc $p \colon \mathcal{E} \to \mathcal{B}$ that has enough opcartesian cells, if $\mathcal{B}$ is representable (i.e. a double category) then $\mathcal{E}$ is too. In the following, I will talk about opfibrations of vdcs for functors with all opcartesian cells.
Before going into the main point some remarks: the category of vdcs and their functors has all pullbacks where everything is defined pairwise (since the functors are strict). A functor of representable vdcs correspond to a lax functor of double categories. And opfibrations of vdcs are closed under pullback.

Nicolas Blanco (Dec 20 2023 at 15:01):

To the main point: one can consider the forgetful functor $\mathcal{U} \colon \mathbf{Dist}_\ast \to \mathbf{Dist}$ from the vdc of pointed distributors to the vdc of distributors, it is an opfibration. There the distributors are the horizontal maps and the vertical maps are functors. Now, given a functor of vdc $F \colon \mathcal{B} \to \mathbf{Dist}$ one can take the pullback with $\mathcal{U}$ to get a vdc $\int F$. Since $\mathcal{U}$ is an opfibration and these are closed under pullback, $\int F$ is opfibred over $\mathcal{B}$. Furthermore, if $\mathcal{B}$ is representable, so is $\int F$. This gives the composition in the Grothendieck construction as a universal property. One can show that some other fibrational properties of $\mathcal{U}$ ensures that when $\mathcal{B}$ is a bicategory or a category so is $\int F$. All of this can of course be done also with $\mathbf{Cat}$ replacing $\mathbf{Dist}$ (which I do in the following).

I think you get graded functors by considering a monoidal category to be a one-object-one-vertical-map representable vdc (i.e. a one-object bicategory). I think what you do is similar, but you don't ask for the category to be monoidal so you get a one-object-one-vertical-map vdc that only has square cells (the codomain is a single horizontal map. It is not representable (but the property of having only square cells will be lifted to the Grothendieck construction).
Instead of considering this embedding of categories into vdcs (where you send objects to horizontal maps and morphisms to cells) one might when to send objects to objects and morphisms to horizontal maps. I think the link there could be done by considering the $\mathbb{E}nd$ construction (generalising the $\mathbb{M}od$ construction). It should take a vdc to its vdc of horizontal endomorphisms. This can be refined to pointed ones by asking for unit cells and to monoids (in the sense of vdcs, so monads) by asking for unit and multiplication cells.

Nicolas Blanco (Dec 20 2023 at 15:01):

Anyhow, there are probably more thing to say but I think this message is already long enough... The main point is that going to vdcs can make the concepts neater, and let one replace "laxity" by "universality". I am curious to know if some of what you all did can be adapted in this language (I will definitely look into it when I have more time). Also it could be interested to look if moving from $\mathbf{Cat}$ to $\mathbf{Dist}$ can give a similar theory for promonads.

fosco (Dec 20 2023 at 15:23):

Now that you appeared in the discussion I remember our short email exchange. At the time, most of your story flew over my head but now it not only makes sense, but feels like you are unraveling some formal content that might be a great help in polishing the theory.

am curious to know if some of what you all did can be adapted in this language

I am also curious. It might be a matter of adapting it, but at the moment I can't see a real obstruction...

Nicolas Blanco (Dec 20 2023 at 16:18):

Yes, I should definitely read the paper carefully to see if anything cries "opfibrations" to me ;)

fosco (Sep 13 2024 at 09:12):

I have been busybusybusy for the last few months.

• https://arxiv.org/abs/2401.04242 A long version of "Automata and coalgebras in categories of species" replaced the conference version, who was written ad usum delphini to please the science-points gods. Now the paper tells the real motivation behind it, which is studying more differential 2-rig theory.
• https://arxiv.org/abs/2408.16581 A paper on fibrations of algebras (finally!) appeared after the long manuscript idled on my personal webpage for almost a year. We have a lot to say about this story, and the paper just scratches the surface of the theory of categorified semidirectness... I gave two (quasi-isomorphic) talks on this matter in the last two weeks (video, slides)
  
• Andrea Laretto, my student, is about to pull a fantastic trick with coends:

image.png

solving, as a byproduct, this old question of mine

Please, give me/us feedback!

Josselin Poiret (Sep 13 2024 at 09:28):

fosco said:

• Andrea Laretto, my student, is about to pull a fantastic trick with coends

I'd love to give feedback on this one but we only have the abstract :)

fosco (Sep 13 2024 at 09:28):

Yeah, we're polishing the last bits in this very moment ;-)

Chris Grossack (they/them) (Sep 13 2024 at 20:31):

I'm also SUPER interested in this directed type theory paper :eyes:. Congrats on all the stuff!

fosco (Sep 14 2024 at 12:34):

In 48 hours this will be on arXiv.
dinat_directed_pre_arxiv.pdf

Enjoy!

Jonathan Weinberger (Sep 14 2024 at 22:30):

fosco said:

In 48 hours this will be on arXiv.
dinat_directed_pre_arxiv.pdf

Enjoy!

Congrats!

Mike Shulman (Sep 15 2024 at 00:48):

This is interesting! I'm a little unclear on what you're saying about semantics in e.g. Warning 2.1. Are you saying that you have a syntax without a semantics that is just inspired by the behavior of dinatural transformations? Or that your syntax does have semantics in a "para-hyperdoctrine" whose fibers are the paracategories of dinatural transformations? Or that you don't actually have a syntax at all, but are just describing the behavior of this para-hyperdoctrine using a notation that looks syntactic?

Andrea Laretto (Sep 15 2024 at 08:33):

Mike Shulman said:

This is interesting! I'm a little unclear on what you're saying about semantics in e.g. Warning 2.1. Are you saying that you have a syntax without a semantics that is just inspired by the behavior of dinatural transformations? Or that your syntax does have semantics in a "para-hyperdoctrine" whose fibers are the paracategories of dinatural transformations? Or that you don't actually have a syntax at all, but are just describing the behavior of this para-hyperdoctrine using a notation that looks syntactic?

Hi, thank you for the comment! We meant the third option: we don't have a formal syntax, and our notation should be interpreted semantically, but we tried to make the notation suggestive of the fact that one can make all of it precise and actually have a formal system. We remark in the end that such a syntax would have a truly compositional model, e.g., in the category of posets where dinaturals compose trivially. The second option you mentioned seemed a bit too imprecise/unsatisfying to us (but it can be done), and the first a bit too ambitious for a directed type theory with just a single model in posets, which is indeed compositional but a bit degenerate; so we decided to instead just present a series of "semantic" results and leave a precise presentation of the syntax (and "directed doctrines") for our next paper, since it can definitely be done and might be something of interest (I have some stuff in Agda ready for this!).

Fernando Chu (Sep 19 2024 at 05:29):

Amazing work! Small question, in the example 5.16 (Yoneda) only naturality on $a$ was shown, right? Does naturality on $P$ follow by putting it on the brackets or does this not typecheck?

Andrea Laretto (Sep 19 2024 at 10:55):

Fernando Chu said:

Amazing work! Small question, in the example 5.16 (Yoneda) only naturality on $a$ was shown, right? Does naturality on $P$ follow by putting it on the brackets or does this not typecheck?

Thank you! Semantically, what you describe can indeed be made to work, and dinaturality in $P$ for the whole map is the naturality in $P$ you're talking about. There is a caveat about size, however: the categories in context $[c: \mathbb{C}, c: \mathbb{D}, ...]$ we consider in the paper are always small categories (they are all elements of $\textsf{Cat}$, the large category of small categories), whereas $\mathbb C \rightarrow \textsf{Set}$ is a large category, since it is a functor category into a large category $\textsf{Set}$, the large category of small sets. In particular, in such a situation you wouldn't even be able in general to compute the large (co)end: a way to avoid this is to make it so that the dinatural transformation itself is taken to be between functors into $\textsf{SET}$, the larger category of large sets (which is large complete). A type theoretical intuition in Agda for this is that, given some type A : Set 0, the type A → Set 0 has itself type Set 1, and if you want to quantify over elements of that type your quantification as a whole becomes a type of Set 2. In a sense you're now quantifying over predicates (presheaves), so you need a way to talk about second-order logic. I hope this helps!

Andrea Laretto (Sep 19 2024 at 11:00):

fosco said:

In 48 hours this will be on arXiv. [...]

(By the way, the arXiv version of the paper is out! Some typos fixed, so thanks to everyone who helped!)

https://arxiv.org/abs/2409.10237