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: Sheaves and operads/multicategories

Spencer Breiner (Jul 20 2023 at 12:32):

I'm curious about the relationship(s) between sheaves and (colored) operads.

It seems like like a site $(C,J)$ should define an operad with objects from $C$ and morphisms from $J$. Then a sheaf $F\in \mathrm{Sh}(C,J)$ would give an algebra determined by gluing.

I would be happy to hear about elaborations on this basic setup (or why this isn't a useful perspective). Clearly this isn't the whole story given that restriction maps haven't made an appearance.

I'm also interested in other touchpoints (like this one that I haven't dug into yet). Thanks!

Spencer Breiner (Jul 20 2023 at 12:35):

Some background: I've been thinking about a topic recently from a sheaf-y perspective and came across a nice reference attacking a similar problem from an operadic perspective. Thinking about how to transfer or extend those results made me wonder about the relationship more generally.

Spencer Breiner (Jul 20 2023 at 12:39):

I would also be interested in relationships that point the other way. Some operads, like wiring diagrams, have a very geometric flavor and I would be interested in constructions for turning these into spaces (perhaps for computational purposes).

Matt Earnshaw (Jul 21 2023 at 12:08):

How is the induced operad defined?

James Deikun (Jul 21 2023 at 12:45):

Well, presumably you can reverse-engineer it from the sheafification monad, provided such a $C$-colored operad exists. I feel like it's going to only exist in relatively rare cases, because generally a cover is going to have overlaps and the gluing operation for a nontrivially overlapping cover should have a sort of arity only found in an [[essentially algebraic theory]]. Besides the gluing operations, it will have restriction operations that equip algebras with the structure of a presheaf of $C$, rather than just a $\mathrm{Ob}(C)$-colored set.

Matteo Capucci (he/him) (Jul 27 2023 at 15:14):

That's a very interesting question Spencer

Matteo Capucci (he/him) (Jul 27 2023 at 15:17):

To me it looks like a site $(\mathcal{C}, J)$ defines an operad $\mathcal{O}_{(\mathcal{C},J)}$ whose objects are the same of $\mathcal{C}$ and whose operations are $J$-coverings. That is, $\mathcal{O}_{(\mathcal{C},J)}(U_1, \ldots, U_n ; X) = \{\{f_i : U_i \to X\} \in J\}$

Matteo Capucci (he/him) (Jul 27 2023 at 15:23):

Which is what you've written too I guess

Matteo Capucci (he/him) (Jul 27 2023 at 15:50):

It's not clear to me how to define a sheaf as an algebra. You have an $\mathcal O_{(\mathcal C,J)}$-algebra $F$ giving you a set for every object of $\mathcal C$ and then for every covering family $f:U_1, \ldots, U_n \to X$ you'd need a map $F(U_1) \times \cdots \times F(U_n) \to F(X)$. But glueing defines such a map only on a subset of the domain -- compatible families of sections.
You do get a map in the other direction, given by restriction though.

James Deikun (Jul 27 2023 at 15:52):

Matteo Capucci (he/him) said:

To me it looks like a site $(\mathcal{C}, J)$ defines an operad $\mathcal{O}_{(\mathcal{C},J)}$ whose objects are the same of $\mathcal{C}$ and whose operations are $J$-coverings. That is, $\mathcal{O}_{(\mathcal{C},J)}(U_1, \ldots, U_n ; X) = \{\{f_i : U_i \to X\} \in J\}$

I guess that is an operad, but the significance confuses me. Forgetting about restrictions for the moment, it also leaves out all the infinite coverings. And the algebras of this operad don't seem to do anything in particular. In particular, sheaves only give partial algebras because the arity of the operad's operations doesn't enforce matching on overlaps.

Matteo Capucci (he/him) (Jul 27 2023 at 15:59):

The finitariety doesn't scare (should it?), I see no harm in allowing the operations to have infinite arity

Matteo Capucci (he/him) (Jul 27 2023 at 15:59):

The rest of the things you say is true, but still... one can ponder

Spencer Breiner (Jul 27 2023 at 20:35):

Agreed that the "algebra" I wrote down won't work without doing something drastic (e.g., replace Set by partial functions). Thanks for the replies!

@James Deikun wrote something interesting about using essentially algebraic theories to characterize the compatibility requirements, but I didn't quite follow. Is the idea to replace the list monad in the construction of multicategories by something fancier?

James Deikun (Jul 28 2023 at 17:15):

Basically you can read the [[essentially algebraic theory]] off of the description of sheafification as a [[left exact]] reflection on the presheaf category. It might still be a very high arity theory though.

Matteo Capucci (he/him) (Jul 31 2023 at 12:37):

Spencer Breiner said:

James Deikun wrote something interesting about using essentially algebraic theories to characterize the compatibility requirements, but I didn't quite follow. Is the idea to replace the list monad in the construction of multicategories by something fancier?

To add to James' answer (and he will correct me if I'm wrong), the idea is to see a sheaf as an algebraic structure with operations whose arities are given by the covers. For instance, if I had a cover of $X$ given by two disjoint opens $U_1,U_2$, then this means the corresponding algebraic structures will come with a 'glueing operation' of type $FU_1 \times FU_2 \to X$. If all covers were disjoint like this, then all the glueing operations would be of algebraic type ([[algebraic theory]]), i.e. the domains would be simply products (bc the compatibility conditions for disjoint covers are trivial). In general covers overlap though, so one's theory of glueing is only an [[essentially algebraic theory]], whose operations have domain which can be arbitrary finite limits (IIRC), such as the pullbacks defining the compatibility conditions for the glueing data of a sheaf.

Matteo Capucci (he/him) (Jul 31 2023 at 12:38):

So I guess the idea here would be to associate to every site its 'essential algebraic theory of glueing', whose operations are glueing of covers in the topology of the site. Then a model for this theory would be exactly a sheaf on the site we started from.

Matteo Capucci (he/him) (Jul 31 2023 at 12:43):

James Deikun said:

Basically you can read the [[essentially algebraic theory]] off of the description of sheafification as a [[left exact]] reflection on the presheaf category. It might still be a very high arity theory though.

This isn't very clear to me, @James Deikun. The localization should give the models of the essentially algebraic theory (EAT) we are after, but how does it give me the theory itself?

James Deikun (Jul 31 2023 at 18:36):

Via [[Gabriel-Ulmer duality]].

Matteo Capucci (he/him) (Aug 01 2023 at 09:16):

uhm so the idea is that a topos of sheaves is locally finitely presentable, hence by duality we get an EAT it is the category of models of?

Matteo Capucci (he/him) (Aug 01 2023 at 09:16):

that's so cool!

Morgan Rogers (he/him) (Aug 01 2023 at 09:31):

But toposes of sheaves are not locally finitely presentable in general...

John Baez (Aug 01 2023 at 10:13):

Locally presentable means locally $\kappa$-presentable for some regular cardinal $\kappa$. Does Gabriel-Ulmer duality, the contravariant equivalence between

• the 2-category of finitely presentable categories

and

• the 2-category of finitely cocomplete categories

generalize to the $\kappa$-presentable case?

If so Matteo's idea should still work.

John Baez (Aug 01 2023 at 10:14):

(When I have time I add links explaining some terms to make it a bit easier for beginners to jump aboard the conversation. Very often I myself am one of these beginners: e.g. I'm no expert on Gabriel-Ulmer duality though I get the basic idea.)

Nathanael Arkor (Aug 01 2023 at 10:23):

John Baez said:

Locally presentable means locally $\kappa$-presentable for some regular cardinal $\kappa$. Does Gabriel-Ulmer duality, the contravariant equivalence between

• the 2-category of finitely presentable categories

and

• the 2-category of finitely cocomplete categories

generalize to the $\kappa$-presentable case?

If so Matteo's idea should still work.

Yes:
Nathanael Arkor said:

Yes, this follows from the general duality theorem of Centazzo–Vitale's A duality relative to a limit doctrine, where the limit doctrine $\mathbb D$ is chosen to be the doctrine of $\kappa$-small limits (see Adámek–Borceux–Lack–Rosický's A classification of accessible categories).

Nathanael Arkor (Aug 01 2023 at 10:24):

The restriction of Gabriel–Ulmer duality to Grothendieck toposes was explored in the paper Gabriel-Ulmer duality for topoi and its relation with site presentations by @Ivan Di Liberti and @Julia Ramos.

John Baez (Aug 01 2023 at 10:46):

Thanks!

dusko (Aug 01 2023 at 16:43):

John Baez said:

Locally presentable means locally $\kappa$-presentable for some regular cardinal $\kappa$. Does Gabriel-Ulmer duality, the contravariant equivalence between

• the 2-category of finitely presentable categories

and

• the 2-category of finitely cocomplete categories

generalize to the $\kappa$-presentable case?

If so Matteo's idea should still work.

FWIW, the Gabriel-Ulmer duality extends to the duality of $\kappa$-accessible categories and sketches with limit and colimit cones of size $\kappa$. This is worked in the Makkai-Pare book on accessible categories, also earlier but in less detail by Lair in Diagrammes. This is the most general version of functorial semantics: basically the functorial semantics for all of infinitary first order logic. The finitary version was in a paper by Adamek, Johnstone, Makowski, and someone (whose name i stupidly forget)...

the reason i studied this recently is that you have this universe of everything that can be expressed in first order logic, formalized as a 2-category, and this universe is in a formal sense computable because the theory of sketches is a first order theory, i.e. sketchable. the sketch of sketch morphisms and dually of the model morphisms can be viewed as a programming language, making everything in this universe computable. so while every static theory expressive enough to encode its own formulas is incomplete, per goedel, applying the computable fixpoint constructions on first order theories we can always construct theories that confirm previously false statements. so dynamic logic supports, in a sense, the opposite of goedel's incompleteness theorem, and this arises from general functorial semantics, just a step above the lfp-theories and the geometric theories. i think the construction even applies to geometric theories alone, ie on the 2-category (actually bicategory) of toposes, but i didn't work that out. it all got conjectured by my daughter, observing how people construct new theories to confirm old lies:
https://arxiv.org/abs/2303.14338v2

John Baez (Aug 01 2023 at 16:52):

Cool!

dusko (Aug 01 2023 at 16:58):

... Adamek, Johnstone, Makowski, and Rosicky of course :)

Steve Lack (Aug 01 2023 at 23:38):

It is true that a category is accessible iff it is sketchable. But the case of $\kappa$-accessible categories for a specific $\kappa$ is not straightforward, as in the locally presentable case, and in particular does not correspond to ketches with limit and colimit cones of size $\kappa$.

Also, I don't know how to make the correspondence between accessible and sketchable categories into a duality, in the sense of a contravariant biequivalence of 2-categories, in a non-tautological way. What are the morphisms of sketches? You can define them to correspond to accessible functors between the categories of models (this or something like it is what I mean by tautological), but otherwise what do you do? There can be many sketches for the same accessible category.

Steve Lack (Aug 01 2023 at 23:43):

Regarding the original question about sheaves and operads, it might be worth looking at the notion of operadic category due to Batanin and Markl. This has a framework in which one can see presheaves as operads. There might be a way to incorporate a topology into the setup. (Full disclosure: I haven't looked at this in a while, and it's very possible that this just doesn't work.)

dusko (Aug 02 2023 at 01:56):

morphisms of sketches were studied by bastiani and ehresmann in their 100 page paper from 1972. then coppey and lair proceeded to generalize these morphisms to capture the functors between the corresponding accessible categories. (the correspondence is certainly not straightforward, as it is not even the case that the sketch cones capture the universal quantifiers like the cocones capture the existential, as lair and guitart immediately showed.) then makkai and pare spelled out the model theory of sketches more precisely, and then makkai proceeded to study the model theory of sketch morphisms in a series of papers, which i think appeared at some point in JPAA. he also had a paper on stone duality for first order logic, not in terms of sketches, and was going to put it all together into a generalized GU-duality (as i think explicitly announced in the book) --- but got tired of it all. it is difficult to present genuinely new results in the world full of reviewers who believe that the party line that they have learned by heart completely explains the world and that everything that looks like they didn't know it must be either wrong or trivial.

dusko (Aug 02 2023 at 02:02):

Steve Lack said:

There can be many sketches for the same accessible category.

that is precisely why the computational constructions apply in this framework. there are many type-checkers for each type, many programs for each computable function, many oracles for each degree... infinitely many in each nontrivial case.

dusko (Aug 02 2023 at 02:24):

aha, i remembered a more direct answer than to send you to bastiani and ehresmann and foltz and lair for morphisms.

Steve Lack said:

What are the morphisms of sketches? You can define them to correspond to accessible functors between the categories of models (this or something like it is what I mean by tautological), but otherwise what do you do?

think of sketches as software specifications and their models as implementations. the morphisms between the implementations are the meaning preserving interfaces (aka the software connectors).

a vanilla interpretation of software specifications maps signature to signature and axioms to axioms. but there are of course very few such things. you want to be able to map the terms of $A$ to derived terms of $B$ and that should map the axioms of $A$ to theorems of $B$. but that is precisely an interface between the models! spelling out the "tautological" correspondence between the model morphisms and the theory morphisms is the heart of functorial semantics.

Steve Lack (Aug 02 2023 at 03:43):

Hi Dusko. That does indeed sound like what I was calling "tautological". Of course almost anything in mathematics can be seen as tautological if you look at it from the right (wrong?) point of view.

With regards Makkai duality, as I understand it, this is not (as you say) done in terms of sketches; nor does it involve accessible categories. At least in the general case, it relies on knowing more than just the category of models in order to reconstruct the theory. That is where the "ultracategories" come in.

For some fragments of logic, this is not necessary. For example, you can recover a Barr-exact category from its category of models.

dusko (Aug 03 2023 at 00:50):

Hi Steve. I got covid. While the RNA viruses are still unlikely to spread through chat lists, the brain fog might. So beware of the following clarifications :))

re the TAUTOLOGY. A tautology is a statement provable from logical axioms alone. But concepts and notations have to be defined, and the definitions are used in the proofs of tautologies. So if on one side we define an algebra as a set $A$ with a family of operations $A^n\to A$ satisfying some equations, and on the other side we have a definition of product-preserving functors and of clones of operations and equations, then the equivalence of categories of algebras and categories of product-preserving functors from corresponding clones is proved from logical axioms alone, by unfolding the definitions. Some deep insights are expressed as definitions rather than axioms, rendering some deep theorems as tautologies. I think Wittgenstein was writing about such things. Moreover, SAT-solvers seem to be telling us that proving tautologies can be hard.

re the DUALITY. I mentioned the functorial semantics of sketches because people were talking about the Gabriel-Ulmer duality --- but Temmie's and my paper does not depend on it. Our constructions are built on one side of this general (albeit tautological) duality: within a universe of logical theories with reference models, as beliefs about the states of the world.

(* People tend to describe their beliefs as first order theories, each with a reference model. General relativity is a first order theory, with the measurements that support it as the reference model. My grandmother's view of WW2 could be written down as a list of first order statements, and the documents that she had about it were the reference model. Her sister might have a different view of the world, and a different reference model. They interpret each other's first order theories, and reconcile the assignments to their respective reference models through some communication interface. Now if we present their first order theories as sketches and their communication interfaces as morphisms, we have a category. Doug Smith and Peter Pepper and I wrote some of this up in some automated software engineering papers from 2000s. A tool based on this was built and they built real software systems using also wrote some papers against all odds... *)

The new insight is that this universe of logical theories is programmable, because there is a logical theory of logical theories. That theory can be used as a programming language (viz a universal machine). We spell out some some program schemas people developed for programming influence and for lying.

It seemed convenient to present this universe in terms of sketches. But every computable function can be programmed in infinitely many ways, every model is described by infinitely many theories, and every theory is a model of the theory of theories in infinitely many ways. So our theory of the theory of theories can be formalized in infinitely many other ways besides sketches. Maybe we should rework the story.

But any reworking will probably fit under teh high-level view in the slides we used at WoLLIC: https://www.mathstat.dal.ca/wollic2023/ (also tutorial, which was a bit of a laugh)