View source for Transcript/Arkor - The formal theory of theories

=SPEAKER A=

So the next speaker is ######### ##### and he knows about the formal theory of theories. Please go on.

=SPEAKER B=
Thank you very much. I'd like to start just by thanking the organizers of the conference for arranging it, especially during these very difficult circumstances. I'd like to thank them also for giving me the opportunity to speak today. So I'm going to start directly with the motivation to recall that an algebraic theory is an identical objector from the free category with strict finite code products and a single object that strictly preserves finite code products. And this category f here is equivalent to the skeleton of the category of finite sets and functions. Now I'm going to be using the original definition in terms of code products, rather in terms of probe rather than in terms of products as is typical nowadays. But you can just dualize and everything will be familiar. Recall also that a co limit in set is Sifted if it commutes with finite products and a monad onset is sifted coconuce if it preserves sifted co limits or if the underlying endofrent observes sifted co limit. And these are exactly the same as finitary monads on set. Now it's well known that these two categories are equivalent and this is an observation that essentially dates back to ###### in the 1960s. Now this tells you that the correspondence is very old and so by now it's very well known. However, despite this it still remains somewhat mysterious. And this is really the motivating question for today's talk. It's why is there a correspondence between algebraic theories and Monance? We'd like to see the connection in such a way that it becomes almost obvious that they should be related. And to do this I'm splitting the talk into two parts. So in the first part we're going to be talking about the classical monarch theory correspondence, the one between algebraic theories out of ##### and #### three monas onset. And this is joint work with ##### #########. And in the second part of the talk I'm going to be talking about how we can consider this perspective in a more general setting, in the setting of a two categories of Nice structure. So we can reenact the correspondence and prove the classical one of the correspondence of a special case as well as other correspondences that appears in the literature. So we'll start with a classical setting. So you want to draw some bridge between algebraic theories and monads. And to do that we're going to introduce a new component which is the concept of relative monad. Now a relative monad is a generalization of a monad from an endofunctor with structure to some arbitrary function with structure. So we're going to fix some function J from A to E and this is going to act a bit like the identity function for our monad. Now, I'm not going to go into the definition in detail. It suffices to know there is a definition and in particular when we take JT identity, this is just the same as a monad. So you can think of it as some skewing of a monad in some sense to an arbitrary factor or an endofactor. Now, every monad is induced canonically by two injunctions, the Kleisley junction and the island bog more junction. And similarly every relative monad is induced canonically by two relative junctions, the Kleisly relative junction and the islandbug more relative junction. And these are respectively initial and terminal in the categories of relative junctions inducing the monad. Now, what's the relative injunction? Well, it's very similar to an ordinary junction. You can see at the bottom we have this onset isomorphism. So we have an isomorphism or a correspondence between morphisms from LX to Y and morphisms from JX to Ry. And so notice if we take j to their density here, this is the same as an ordinary injunction. But now we sort of skewed the injunction relative to this function j, which was fixed. And so we're going to denote this with this triangle diagram in the center. So from the universal properties of the ##### and ########## ##### junctions we have the following in byjection j relative ######, j relative clyphy resolutions and j relative ####### more resolutions. And by resolution I mean a pair of functors L and R that are j relative adjoining to one another and composed to give the monad and have the initial internal universal properties. So in this talk in particular, we've been fixed on just these first two. Now, the important point which makes this perspective even possible is the following characterization of CLIC inclusions. So we have a characterization of when a functor is the same as a functor as inclusion of a category into the Kleisley category for some relative monad. So a function K from A to B is the Kyce inclusion for a j relative monad if and only if it has a right j relative adjoint and it's the identity and objects. And in particular, this second point should look familiar because being an identical objects factor is one of the properties of an algebraic theory. The other property is a column preservation property and we're going to see how that fits in just a moment. So first I'm going to talk about relative injunctions that are relative to the inade embedding. So consider some function from A to B and we're going to say that the domain is small. To simplify things, in this case we have an injunction relative to the Yanadri embedding of A where the left adjoin is given by F and the right adjoint is given by the nerve of that. And in this way we can see that every suitably small functor is left adjoint relative to the Nadri embedding of its domain. And conversely, every left adjoint relative to a unitrine bedding is just a small functor. So being a left eye joint relative to the neighboring bedding is not a very strong property at all. However, things get more interesting when we consider co limits. So if F additionally preserves some class PSI of co limits, then this adjunction on the previous slide restricts to a rotator junction where we take the preseaves that preserve PSI columns and in particular every small function that preserves finite coproducts. Assuming here that the domain has finite coproducts is left adjoining relative to the inclusion into the finite product preserving preseaves on A. And this is equivalent to the inclusion into the sifted cocompletion of the category A and it turns out the converse also holds. So every left adjoint relative inclusion into the sifted cocompletion preserves finite coproducts. And so really we think of these as the same thing and this is an analog of the adjoining function. So now we can say that an algebraic theory is equivalently an identian objects functioner that strictly preserves finite coprolux from F or it's an idention objects functioner which is left adjoint relative to this sifted genetry embedding or it's the cliff inclusion of a monad relative to this sifted enatrium bedding. And this way we can tell the algebraic theories are in bijection with monads relative to the sift and unitra embedding. And just a little bit more concrete, this sifter unit embedding is precisely an inclusion of F intercept or the inclusion of finite sets and functions into the category all sets. So now we have a connection between algebraic theories and relative monads which are given by this kaisely characterization, as well as this relative adjoint colon preservation property. So now we're going to try to draw a connection between relative monds and monads and we can also do this. So we're going to fix a class phi of weights and we think of phi as being some class of Coleman diagrams essentially. And then there is an equivalence of categories between the monads relative to the embedding into the phi cocompletion on some category A and the category of phi coconuced monads on the phi cocompletion of A. And in the setting we're interested in we have that monds relative to the embedding into the sifted cocompletion of F are equivalent to the sifted coconuced monads on a sifted cocompletion of F, which is just the category of sets. So these are the same as Finus three monads on set. And hence we have now this equivalence between algebraic theories and monads, which is very elementary in a sense. In particular we haven't made use of any monadisti argument. It proceeds directly from the definition of algebraic theory and from monad. Now, because I haven't mentioned the algebra's at all since I haven't used any kind of monarchisty argument, for instance, you may be wondering what's happened to them because in the classical monet theory correspondence we say that an algebra for a monad corresponding to an algebraic theory is the same as a model for the algebraic theory. So this equivalence between algebraic theories and monads commutes with the process of taking algebra as models. Unfortunately, I don't have time to talk about this right now, but I'm very happy to have you asked this during question time and I can go into a little more detail about it. Okay? So now for the second part of the talk, I'm going to show how we can use this new perspective on the monetary correspondence by relative one adds to reenact the similar argument in an entirely formal setting. So we'd like to know what the most general setting we can carry out this argument is and why do we want to do this? Well, there are many instances of monotherapy correspondence in the literature and really we'd like to know that they all follow from a general theorem because they all have the same shape. They all should be instances of the same phenomenon. As examples, we have monetary correspondences for enriched categories such as that of ###### ###### and of ###### #####. We have correspondences for internal categories such as that of ####### and ####. And we have correspondences for infinity one categories such as those of ########## and ####### #######. So it would be nice if all of these could be shown to follow from some general argument. Now, the setting we're going to be working in is this. And I'm going to state the main theorem and I'm going to deconstruct the assumptions that we have and the definitions. But this will give you an example to keep in mind. So we're going to let K be a two category with a factorization system which we call resolute. And I'll explain what resolute means in just a moment. And I'm going to let Phi be a fully faithful lax IDM voted pseudomonas on K. And this intuitively acts as a cocompletion pseudomonad. Another name for this is a ksed doctrine. I'm going to fix some object A of our two category. Finally, we're going to suppose that every monad relative to the unit of the pseudo monad A has a resolution. And this means that for every ETA a reserve monet, there is some ETA a reserve junction inducing that monet. In this case we can show that there's an equivalence of categories between the theories relative to E to A and the phyco continuous mona's on fi of A. I'm going to tell you what these definitions are in just a moment. But the example to keep in mind is when K is the two category of categories, the factorization system is the identical and objectively facial factorization system. Phi is the pseudomonas for sifted cocompletion and A is the category F. So the three category finite code products on a single object. And yeah, in this case the equivalent to the bottom of the slide will be the classic monet theory correspondence. Now again, we want to prove this theorem by splitting into two parts by drawing this connection with relative monads. Now, the theory of #####'# in a two category is well known and the theory of relative monet and a two category is recently initiated by lobbya. And this is the definition we'll be using. I'm not going to actually give you the definition in the talk because it takes a little while to set up. But suffice to know there is a definition relative monitor in a two category which specializes to the usual notion of relative monet, one k is capped. Okay? So I'm going to explain what a resolute factorization system is, which is really the definition that makes this work. So we're going to select KVA to capture the factorization system. And by factorization system I mean essentially an orthogonal factorization system. But whether the factorization is just up to unique, up to isomorphism, I'm going to say that the factorization system is resolute if every factorization of a one cell into e followed by M satisfies, the property that e is left adjoin to m relative to the composite em. Now this probably looks like quite a funny property, it's probably not very intuitive. So let me give you the reason why this is useful. So if you look at the diagram to the bottom of the slide, what this property means is that if we have any J relative a junction for any J, so l is left our joint R relative to J. And we factorize the left adjoint into e, followed by M. Then, if the factorization system is resolute, we can shift M over to the right hand side. Then E is left Adjoin to M followed by R. So a resolute factorization system essentially allows us to shift M cells from one side from a relative junction to another. So now again with k, a two category with factorization system which are now asking to be resolute, we're going to fix some J one cell and suppose every Jredom monet is a resolution. So for every J relative monitor there is a J rental junction that induces the Jreiter to monitor. Now we define a J theory to be in an e cell that is a left J relative adjoint. And in this case we can prove there's an equivalent of categories between the J theories and the J relative monet's. Now I haven't defined the morphisms of these categories here, but they essentially are the same as the classical setting. Now the proof of this is very similar to the proof in the classical setting. Essentially what this resolute factorization system allows us to do is show that the e cells that have this property characterize the ##### inclusions for JRE monds. So this gives us the connection between theories and relative monds given by this ##### characterization. It's now between relative monies and monds. So this works very similarly to the classical setting. So in J is the component of the unit. So e to A, of a fully faithful, laxide, impatient, pseudo monet, then we have an equivalence of categories between the monads relative to the unit today and the five co continuous ###### on Fire Bay. And by composing with the equivalence on a couple of slides ago, we have that the theories relative to E to A are the same as five copontunist monads on five A. And so this completes the monad theory correspondence in the two category. And although I've skipped the proofs, they're actually very elementary and follow from the same sort of reasoning as in the classical setting. So really once you have the definitions, things work out very nicely. I should mention briefly that some of you may be wondering what happens to monad theory correspondences where we have more general J. Because here I've just concentrated on when J is a component of a fully faithful ######### pseudomyd. So when the monads are given by some colon preserving monads. And although most correspondences in the literature are of this form, there are some correspondences that aren't. And so it's an interesting question to ask about more general J. And again, I don't have time to go into this now, but I'll be happy to answer questions about it later. But in short, we can also get the correspondence more general J which takes a little bit more work and it's a little less clean. So I'm going to use the last few minutes to talk about some examples. The first question you might have is how common are these factorization systems which are resolute? And it turns out it's not a very strong property to impose. In particular, any factorization system for which each M cell is represented to be fully faithful is resolute. And we have a whole class of examples given by the Pro Arrow equipments with finite type collages. These are prior equipment satisfying axioms four and five of woods priorities two and they're the prior equipments that are particularly well behaved. And so any such prior equipment has a factorization system called the Surge Action Inclusion Factorization System. And this is an example of a resolute factorization system. And so if we take the prior equipment as categories into pro factors, this gives us a Bijective and objects fully faithful factorization system. I just quickly want to note that it doesn't matter really whether we take identical objects factors or bijective objects factors. There's just a slight difference in strictness. But the argument works in the same way and the simply works for enriched categories. So to be slightly more concrete, let V be a Bicomplete closing noidal category. Then we have the VCAT. The two category has a resolute factorization system which are given by the identity and objects Vfunctors and the fully facial Vfunters and has resolutions of relative monarchs given by what both the Kaiser and the ######### more V categories. In this case we recover a relative monad theory correspondence. So essentially in all settings we have a relative monot theory correspondence. They're essentially the same thing. And when J is nice this extends to a monop theory correspondence. So in particular when we take j to be the cocompletion. Under a class of weights for V, we recover the monotheory correspondence of ###### right. And when we take J to be a dense, fully fatal functional with small domain and low tube sensible codomain, we recover the monothery correspondence of ##########. So though this two categorical setting may seem very abstract, we can actually use it to deduce general correspondences in concrete settings that we're interested in. Now, I'm going to wrap up here, which will give us enough time for questions. So the sort of key idea that underlies this perspective is that algebraic theories are precisely the closing solutions of relative ######. They're the same thing. There's no difference between them, they're just a different way of writing down the definition, essentially. And from this we can choose the monad theory correspondence by extending relative monas to monads. And this is the step that needs some assumptions. So this is why we often work with J to be the unit of a cocompletion because this is a nice setting from which there's always a monet correspondence with router monads. And this argument is very neat. It doesn't require any complex hypotheses, so it can be carried out in any two cascade with some nice structure and namely this resolute factorization system and fully fatal oxide of major pseudomyde. And then the invictional Napperia correspondences follow special cases and it's ongoing work to check that the internal correspondences and the higher correspondences also follow from the same arguments. I'm going to leave it here and I have references on the slide that these slides will be online so you can check them later. Now I'll be happy. Any questions?

=SPEAKER A=
Thank you for this very interesting talk. The questions or comments first from the audience.

=SPEAKER C=
Thank you #######, for your beautiful talk. I have two comments. The first one is that your definition of resolute reminds me of the notion of your nether triangle by that Polish guy. I don't remember his name, but I think you know what I'm talking about.

=SPEAKER B=
I know you're talking about, yes.

=SPEAKER C=
Thank you. And he has this notion of Yoneda triangle which reminds me of one of the definitions you gave. And then the second comment is that a good test for this framework you develop, but could be really these restriction categories where we have the notion of partial of your theory and we don't know whether there is a factorization system like yours nor a KV doctrine like the one you want. But it's perfect because that is an honest two category which is very far from B v cut for some B. So it could be a test place and maybe we finally discovered that there is no monot correspondence. I don't know. Or maybe there is.

=SPEAKER B=
Thank you for those comments. Yeah, they're helpful. I can comment briefly on the second point which is that restriction categories were one of the motivations for the two categorical spective because as you say, it's a very interesting question and I've worked out some of the details. The problem is there's still some theory of restriction categories that needs to be worked out. In particular, we need to know whether there is a completion of restriction categories. We know there's a co completion, but we don't know whether there's a completion. And so if we know there's a completion, then we can use some of these arguments. But that still needs to work out. I think it's a very interesting direction. Yeah.

=SPEAKER A=

Okay, thank you very much for this very interesting talk. I was wondering that how you framework in some of the monad connect with either ######## and ###### on sound doctrines and in particular how if you can.

=SPEAKER C=
For instance, characterize.

=SPEAKER A=
The ##### which correspond to the case ##### in which would correspond to sound doctrine and also how the algebra structure for different theory would be connected to being flat in the context of being here.

=SPEAKER B=
Yeah, thank you for those questions. Good one. So one thing I didn't mention in the two categorical setting, because I didn't have time, is that well, in the classical setting we have a correspondence between adjoints and colmit preserving functions and we'd like to set something similar in the formal setting. And so it turns out we can do this and in some work in progress with Evangeliberty and Foster Lesion, we have a relative adjoining theorem in a two category. And in this setting we can show that certain theories in the two category correspond to co continuous one cells in a certain sense. So this is how we recover that in the two category. And so in particular, when we take sound limit doctrines, we get such a nice situation. And so we have a correspondence that works the same way as this framework you mentioned. And I very briefly mention how it relates to the categories of models. We have this characterization of the category of algebras for a relative monad in terms of a pullback over the Kiosky category or precise on the Clicy category. So this pullback probably looks quite familiar to anyone who studied monad theory. Correspondences is a definition of the cattery of models for various classes of monads and it turns out this is a characterization of the category values for relative monet and this is how it connects to the correspondence perspective I outlined. And in particular, when we take an algebraic theory which corresponds to some relative monad, then we can evaluate this pullback. And so I'm going quite quickly here, but essentially if we work out what everything is concretely, we can show that the category of algebra is for the relative monet corresponding to an algebraic theory is equivalent to the finite product preserving functions from the codomain, which is the quiet category of the algebraic theory intersect. And so this is the sort of approach we can use to capture the setting you were talking about of these limit preserving funters and sound doctrines.

=SPEAKER A=
Okay, we have questions from the audience. ####. Not from the audience, non audience, ####.

=SPEAKER D=
Arkor, you seem to have a pretty powerful and modern piece of machinery there. Now, since you're so keen on looking at old papers, you probably know what I'm about to say. It looks like your relative adjunctions and monarchs. So they presumably take account of multi and polyad joints and therefore DS disjunctive theories. And when I was involved in that kind of thing, I was brought up by one of the Perry Set people, ######### ##### running guitar, or one of them who said, oh, well, we have adjoining for any funk. So I would imagine that you would have a modern point of view on some of the stuff that they did.

=SPEAKER B=
Yeah, thanks for that. I can briefly comment. So one of the other Motivating samples.

=SPEAKER A=
Which I didn't mention before you briefly comment, let me briefly comment that we are really over the time and we were all less strict on the time, and somehow it's not fair to the other ones. So please comment really briefly.

=SPEAKER B=
Yeah, one or two sentences. So, yes, diaz multimonats and things like this were another Motivating example, and in fact, I mentioned in my abstract, but on the talks, I didn't have time and there is a relationship, but it's a little more complicated than I have time to start out now. But, yes, I hope to give treatment of that as well. So thank you for that comment.

=SPEAKER A=
Thank you. And may I suggest that if there are and there are, namely some other questions that may be answered on the Internet and not physically, because our time is simply out, nonetheless, we will have a three minute break and start three minutes later and stop three minutes later. Of course.