Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 11, 2009

Report on 88th Peripatetic Seminar on Sheaves and Logic

Posted by Urs Schreiber

guest post by Mike Shulman


Hi everyone! Urs invited me to update everyone on the highlights of the PSSL 88 in Cambridge, U.K.

One of the highlights for me was meeting people who I’d previously only known virtually, including some nStuff patrons like Bruce Bartlett, Finn Lawler, and Ronnie Brown. I would also be remiss if I didn’t give honor to Peter Johnstone and Martin Hyland, in recognition of whose 60th birthdays the conference was being held; I met them both when I was doing Part III in Cambridge and was very inspired by them. There were also lots of great talks, which I’ll try to summarize; also, I think that some slides will be posted eventually.

First, Dana Scott talked about models for modal logic. He started by recalling the definition of a complete frame-valued set, an alternate way to construct the category of sheaves on a locale. Then he proposed to replace the frame (= complete Heyting algebra) by a complete Lewis algebra: a complete lattice LL equipped with a lex comonad \Box (that is, 1=1\Box 1 = 1, x=xx\Box\Box x = \Box x \le x, and (xy)=xy\Box(x\wedge y)=\Box x \wedge \Box y). With this he defined an intensional map of complete LL-sets to be a function ff which preserves extents |fx|=|x||f x|=|x| and such that [x=y][fx=fy]\Box [x=y] \le [f x = f y]. I guess this means that it only preserves “necessary” or “definitional” equality rather than “contingent” or “extensional” equality as the condition [x=y][fx=fx][x=y]\le [f x = f x] would require. This defines a supercategory of the category of sheaves on LL, and one can then investigate and attempt to axiomatize its properties as a “modal version of a topos.”

Then Richard Garner talked about topological models of type theory. It looks like type theory has come up a few times in passing on the nCafe but never been discussed in detail, so I thought it would be worthwhile writing a brief introduction. But rather than posting it here, I decided to put it over at the nLab. So go read that and then come back here.

Back? Okay, one thing I didn’t mention about the “propositions as types” paradigm (although someone may have added it by the time you read this) is that it gets a bit subtle when you start thinking about equality. In typed predicate logic, equality is given by a particular proposition x= Ayx=_A y for two variables x,yx,y of type AA. Semantically this is usually modeled by an equalizer. In dependent type theory, instead of a proposition x= Ayx=_A y we have an identity type Id A(x,y)Id_A(x,y), which you can think of as the “type of all proofs that x= Ayx=_A y.” Of course, if x=yx=y there may be many proofs of that fact, so Id A(x,y)Id_A(x,y) may not be a subobject of A×AA\times A.

If Id A(x,y)Id_A(x,y) is inhabited (there exists a term pp of type Id A(x,y)Id_A(x,y)) we say that xx and yy are propositionally equal with pp as witness. The rules for manipulating identity types ensure that equality is transitive, reflexive, and symmetric: for instance, we have a term Id A(b,c)×Id A(a,b)Id A(a,c).Id_A(b,c)\times Id_A(a,b) \to Id_A(a,c). and a term Id A(a,b)Id A(b,a)Id_A(a,b) \to Id_A(b,a) and a term 1 a1_a of type Id A(a,a)Id_A(a,a).

Now obviously, Id AId_A is a groupoid, just as the proposition x= Ayx=_A y is an equivalence relation. Well, not quite—it’s a groupoid up to propositional equality! The composition is associative, unital, and has inverses, but only up to propositional equality. You shouldn’t have any trouble guessing that in fact, we have an infinity-groupoid AId AId Id A.A \leftleftarrows Id_A \leftleftarrows Id_{Id_A}\leftleftarrows \cdots. This was apparently observed simultaneously by Garner-van den Berg and by Peter Lumsdaine. By applying the homotopy hypothesis, we conclude that the semantics of propositions-as-types type theory should really happen in topological spaces (or some other equivalent model), with propositional equality modeled by homotopy.

To make this precise, Richard suggested to consider, as a model of dependent type theory, a category CC equipped with a nice weak factorization system (L,R)(L,R). A dependent type B(x)B(x) with xAx\in A represents a map BAB\to A which is moreover required to be in RR; we think of it as a sort of “fibration.” And the identity type Id AId_A represents a path object of AA, given by the (L,R)(L,R)-factorization of the diagonal AA×AA\to A\times A. There are a couple subtleties required to make this work. In particular, you need to assume that the pullback of an LL-map along an RR-map is again an LL-map; this “Frobenius property” “makes the identity types parametrizable.” This is satisfied by the (trivial cofibration, fibration) wfs for the folk model structure on groupoids, which reproduces a model of type theory due to Streicher and Hoffman, but not for the (trivial cofibration, fibration) wfs for the Hurewicz model structure on TopTop unless we use Moore paths (paths of arbitrary nonnegative real length) instead of the usual paths of length 1. One can also try to emulate Moore paths in the simplicial world.

A couple people talked about other aspects of type theory and logic, but the next talk that I understood was by Oliva Caramello, who showed that subtoposes of the classifying topos of a geometric theory are in bijective correspondence with quotients of the theory (theories with the same signature which can prove at least as much). You can then look for correspondences between topos-theoretic properties of subtoposes (open, closed, quasi-closed) and logical properties of the corresponding theories.

Then Nick Duncan talked about the difference between gros and petit toposes, which is a subject that came up here recently. He said that intuitively, the difference is that

  • A gros topos is a topos whose objects have geometrical structure, such as simplicial sets or sheaves on a full subcategory of TopTop, while

  • A petit topos is a topos constructed from a single geometric object, such as sheaves on a single topological space, or GG-sets for some group GG.

Nick argued that taken separately, these notions are fairly vacuous. For example, there are well-known “representation theorems” saying that any (Grothendieck) topos is equivalent to the category of sheaves on a localic groupoid (a groupoid internal to the category of locales) — which is surely a single geometric object. The important thing is the relationship between a gros topos and the petit toposes corresponding to its objects.

Nick presented the following tentative definition: a gros topos is a topos GG equipped with, for every object FGF\in G, a topos P(F)P(F) called the petit topos of FF and a local geometric morphism p F:G/FP(F)p_F: G/F \to P(F), and for every g:FHg:F\to H in GG, a geometric morphism P(g):P(F)P(H)P(g):P(F)\to P(H) and various commutativity relationships, presumably including coherence isomorphisms.

(A geometric morphism is local if its direct image p *p_* has a right adjoint p !p^!.
Then (p ,p !)(p_\star, p^!) is also a geometric morphism, which exhibits P(F)P(F) as a subtopos of G/FG/F, and P(F)P(F) and G/FG/F are “homotopy equivalent” and have the same cohomology.)

We call the topos P(1)P(1) the topos of points of GG; since G/1GG/1\simeq G we have p=p 1:GP(1)p = p_1:G \to P(1). Objects of the form p *(A)p^*(A) are called discrete, and objects of the form p !(A)p^!(A) are called codiscrete. I believe that P(1)P(1) is supposed to function as something like “the topos of sets relative to GG.”

The canoncial example is the Zariski topos kZark Zar over a field KK: the topos of sheaves on the cosite of kk-algebras with coverage consisting of the finite families {AA[a i 1]}\{A\to A[a_i^{-1}]\} where (a 1,,a n)=1(a_1,\dots,a_n)=1. For any kk-algebra AA, we define P(A)=Sh(SpecA)P(A) = Sh(Spec A). For an arbitrary object FF in kZark Zar, we write FF as the colimit of representables, let |F||F| be the topological space obtained as the corresponding colimit of Zariski spectra, and let P(F)=Sh(|F|)P(F)= Sh(|F|). There is a functor O:kAlgSetO:k Alg \to Set that takes a kk-algebra to its underlying set, and for any FF in kZark Zar we can pull back OO to kZar/Fk Zar/F and then restrict to P(F)P(F) to obtain a structure sheaf O FSh(|F|)O_F \in Sh(|F|) making |F||F| into a locally ringed space (and Sh(|F|)Sh(|F|) a locally ringed topos).

Toby Kenney talked about the “free diad” using graphical calculus, in the same way that the algebraic simplex category Δ +\Delta_+ gives the free monad. A diad is a structure that simultaneously generalizes a monad and a comonad; it’s a functor TT with natural transformations α:TTT\alpha:T\to T T and β:TTT\beta: T T \to T satisfying certain axioms. A monad (T,μ,η)(T,\mu,\eta) gives rise to two diads, one with α=ηT\alpha = \eta T and β=μ\beta = \mu, and one with α=Tη\alpha = T \eta and β=μ\beta = \mu. A comonad likewise gives rise to two diads. It turns out that one can define both a category of dialgebras and a di-Kleisli category for any diad, and when applied to the diads coming from a monad or comonad one can recover the usual categories of algebras and Kleisli categories. Also, if TT is any idempotent functor (TTTT \cong T T), then α=β 1\alpha = \beta^{-1} is a diad, and if TT is any diad, then TTT T can be made into a diad as well.

One other thing worth mentioning is that if TT is any finite-limit-preserving diad on a topos which is “distributive” (an extra axiom relating α\alpha and β\beta), then its category of distributive dialgebras is again a topos. This unifies the two classical theorems that the category of coalgebras for a lex comonad on a topos, and the category of algebras for a lex idempotent monad on a topos, are again toposes. It feels quite similar to Todd’s three topos theorems in one, but Toby and I were unable to work out a very precise connection.

Pino Rosolini told us about a construction of an extension of the effective topos. The effective topos EffEff is a topos in which “everything is computable,” although you have to interpret that suitably broadly. It includes SetSet as a full subcategory, so not everything can be computable; however, the natural numbers object NN is not the one coming from SetSet, and every function NNN\to N is in fact computable. Moreover, you can look at all the objects “built from” NN, called modest sets, and all the maps between them will be computable.

Furthermore, it turns out that the modest sets form an internal category PERPER in EffEff, and that internal category is complete. So while it’s true in SetSet that any small complete category must be a poset, this is not true in EffEff. However, making this precise involves comparing the “externalization” of PERPER with the fibration of modest sets, and these aren’t as equivalent as you might like; rather the latter is the stackification of the former. Pino’s talk was about a construction of a topos \mathcal{F}, which logically extends EffEff, and which contains a internal category which is strongly equivalent to the complete fibration of modest sets.

John Power’s talk about generalized Lawvere theories began with a calculatedly inflammatory statement: the emphasis on monads to understand universal algebra is the single worst mistake in the history of category theory. His claim: Lawvere theories are much better. Why? He listed a few reasons.

  • The coproduct of Lawvere theories always exists; not so for monads.

  • The tensor product of Lawvere theories always exists; not so for monads.

  • Calculating a monad from generators and relations is a nightmare, but it is easy and natural with a Lawvere theory.

  • Lawvere theories are also a natural beginning to categorical logic: they are finite-product theories, from which we can move up to finite-limit theories, finite limit and finite sum theories, geometric theories, and so on.

Monads are interesting and useful (said John), but for purposes of universal algebra, Lawvere theories are better. (Note that changing “finite” to a bound of any other cardinality is a trivial variation. It’s only monads having “operations” of potentially arbitrarily large arities, like the monads whose algebras are complete lattices or compact Hausdorff spaces, which don’t fit the Lawvere theory framework.)

However, while one can talk about monads on any category (and in fact, in any 2-category), to talk about Lawvere theories one needs a notion of “size.” John proposed the following framework: if CC is a locally finitely presentable category, a Lawvere CC-theory is a category LL and a functor J:C f opLJ:C_f^{op}\to L that preserves finite limits. Here C fC_f is (a skeleton of) the category of finitely presentable objects in CC. Then a model of LL is a functor M:LSetM:L\to Set such that MJM J preserves finite limits (and hence is representable by an object of CC). Theorem: Lawvere CC-theories, thusly defined, are equivalent to finitary monads on CC (those that preserve filtered colimits).

(My personal take on the question: a monad represents the extensional essence of an algebraic theory, and it’s important to keep in mind both this essence as well as any particularly convenient presentations of it that may exist. There are many such situations where we need to think about one object as a “presentation” of another one, the presentation being non-canonical and not always existing, but easier to construct and manipulate when it does. For example, topological spaces present homotopy types, model categories present (,1)(\infty,1)-categories, sites present topoi, and even group presentations present groups!)

Bill Lawvere then ended the first day by discussing some open problems in topos theory, relating in particular to what he called “quotient toposes” (a stronger notion than just a “surjective” geometric morphism).

The next day, Michael Fourman started off by talking about ways to represent quantales using relations in a presheaf topos. Given a quantale, you can write down a geometric theory describing it as relations, and then in the resulting classifying topos there will be an internal collection of relations representing that quantale.

Ieke Moerdijk gave a nice talk about generalized Reedy categories (“greedy categories?”). I thought that Reedy categories deserved a page on the nLab, so I made one, including a brief summary of the generalization Ieke presented.

Nicola Gambino’s talk on monads in double categories was dear to my heart because he started off by giving the definition of a framed bicategory. He then proceeded to consider a (horizontal) monads in such, but forming a different framed bicategory Mnd(C)Mnd(C) than the one Mod(C)Mod(C) that I studied. Nicola (and Tom Fiore and Joachim Kock) are interested instead in a framed version of the 2-category Mnd(K)Mnd(K) used in Street’s “Formal theory of monads,” where a morphism from a monad s:AAs:A\to A to a monad t:BBt:B\to B consists of a morphism f:ABf:A\to B and a 2-cell ϕ:tffs\phi:t f \to f s satisfying exactly the axioms necessary for ff to lift to a functor from ss-algebras to tt-algebras. Nicola then stated a theorem that if CC is a framed bicategory, so is Mnd(C)Mnd(C). The point was to use the framed structure to make it easier to construct free monads on endofunctors.

The motivating example was polynomial endofunctors, which happen in a generalization of the framed bicategory of spans. Let EE be a locally cartesian closed category; then we have a framed bicategory whose objects and vertical morphisms are those of EE, and in which a horizontal arrow IJI\to J is a diagram IsBfAtJ.I \overset{s}{\leftarrow} B \overset{f}{\to} A \overset{t}{\to} J. We view this as a “presentation” of the polynomial functor E/IE/JE/I\to E/J defined by Σ tΠ fs *\Sigma_t \Pi_f s^*. When J=IJ=I this is intended to be thought of as a “many-sorted signature:” II is the set of sorts, AA is the set of operations, tt assigns the target sort of each operation, the fiber B aB_a is the arity of the operation aAa\in A, and ss assigns a sort to each input. A monad in this framed bicategory is then a polynomial monad, and Nicola stated a theorem that if EE has initial algebras for all these functors, then it admits the construction of free monads.

Dominic Verity then gave a brief tour of the “simplicial approach” to (nerves of) weak ω\omega-categories, which involves defining the simplicial nerve of a strict ω\omega-category, characterizing the things that arise as such nerves, and then weakening the conditions. This was the very first definition of weak ω\omega-category, proposed by Ross Street back in the dark ages, and has since been carried forward, also by Street and others but especially by Dominic.

The idea is, as you probably know, to define the free strict ω\omega-category on an nn-simplex and use that to define the nerve StrωCatsSetStr\omega Cat\to sSet. But (unlike for 1-categories and (,1)(\infty,1)-categories) we can’t expect that functor to be full and faithful; we need to remember which simplices are identities. A collection of simplices, called thin and thought of as being identities (or equivalences), is called a stratification on a simplicial set. The nerve of strict ω\omega-categories is fully faithful to stratified simplicial sets and we can characterize its full image by certain unique horn-filling conditions.

In the strict case, you can’t get rid of this extra structure; one can construct simplicial sets having many different stratifications that correspond to many different ω\omega-categories. For instance, let MM be a monoid, regarded as a chaotic monoidal category (all objects uniquely isomorphic), and deloop it to get a 2-category BMB M. Then its simplicial nerve N(BM)N(B M) is 1-coskeletal, which means that an isomorphism N(BM 1)N(BM 2)N(B M_1) \cong N(B M_2) is just an isomorphism of pointed sets. So you just need to find a set admitting two different monoid structures.

The stratified simplicial sets arising as nerves of strict ω\omega-categories are called complicial sets. If we simply relax the uniqueness of the horn filler (now thinking of thin elements as “equivalences” rather than identities), we get the notion of weak complicial set. But these are not quite yet a notion of weak ω\omega-category, since they might not have enough thin elements. This is clear when you observe that the category of weak complicial sets contains the category of complicial sets, and hence the category of strict ω\omega-categories and strict ω\omega-functors, as a full subcategory; whereas while we can certainly regard a strict ω\omega-category as a weak one, we want to see all the weak functors as well.

One natural thing to do now is to “saturate” our weak complicial sets so that “everything that should be thin is.” This turns out to involve some more difficult combinatorics, but the upshot is that it’s possible. (The proof actually involves showing that weak complicial sets are equivalent to categories enriched in weak complicial sets, the same way that quasi-categories are equivalent to simplicially enriched categories.) So we can think of a weak complicial set as a “presentation” of a weak ω\omega-category, where we’ve noticed enough internal equivalences to show that it is a weak ω\omega-category, but perhaps we haven’t noticed all the equivalences. This is very analogous to the “completion” process applied to Segal spaces.

However, it’s not yet clear to what extent the stratification can be dispensed with entirely. Dominic mentioned some partial results:

  • A simplicial set can have no more than one stratification which is a saturated 2-trivial weak complicial set (everything is thin above dimension 2).

  • Given a saturated nn-trivial weak complicial set, its stratification is maximal among complicial stratifications on its underlying simplicial set.

Aaron Lauda then gave a lovely talk about categorifying quantum groups, but it depended so much on beautiful colored slides that I can’t say anything very coherent about it. The slides will supposedly be here.

Tom Leinster and Apostolos Matzaris spoke together about a new way of constructing terminal coalgebras for finitary endofunctors of locally finitely presentable categories, using distributors. If we write our lfp category as the category Lex(A,Set)Lex(A,Set) of finite-limit-preserving functors on some category AA with finite limits, then any finitary endofunctor is of the form M AM\otimes_A - for some flat distributor M:A op×ASetM:A^{op}\times A \to Set. In this case, the terminal coalgebra can be constructed as follows: T(a)T(a) is the set of connected components of the category of complexes a 3m 3a 2m 2a 1m 1a\dots \to a_3 \overset{m_3}{\to} a_2 \overset{m_2}{\to} a_1 \overset{m_1}{\to} a where m iM(a i,a i1)m_i \in M(a_i,a_{i-1}). The intuition behind this is that T(a)T(a) is the set of “ways in which aa can behave under repeated application of the endofunctor M AM\otimes_A -.”

Julia Goedecke then spoke about satellites in semi-abelian categories. It seems there are many different ways to define such satellites, which work under different conditions and agree whenever they are all defined. One uses comonads (as has been discussed, for instance here), one uses “Hopf formulae,” and one uses Kan extensions. In particular, the latter works without the assumption of enough projectives. Unfortunately, I didn’t understand the details.

Finally, Paul-Andre Mellies spoke about game semantics for proof theory.

Posted at April 11, 2009 11:58 AM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1949

22 Comments & 2 Trackbacks

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Thanks, Mike, impressive report. Very useful.

I am particularly interested in the bit about gros and petit topoi. I need to think about what so you said about that, but not right now, since I am once again in a rush.

But this sounds like it is related to an issue which i still haven’t fully sorted out for myself:

we are frequently interested in nn-sheaves on large sites, such as TopTop or DiffDiff and the interplay of these with those over-category topoi that you mention.

Now, the size-issue is a nuisance. I suppose it means that the topos Sh(Top)Sh(Top) does not have enough points. In the literature on model structure on simplicial presheaves one finds vague remarks that one can look at presheaves on small subcategories of TopTop and that the localization doesn’t really depend on that. I don’t think I have fully understood this the way I ought to.

Posted by: Urs Schreiber on April 11, 2009 1:38 PM | Permalink | Reply to this

Properties of Structures of Stuff; Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Does this “the relationship between a gros topos and the petit toposes corresponding to its objects” yield insights into the Stuff, Structure of Stuff, Properties of Structures of Stuff trinity (he asked, Easterishly)?

Posted by: Jonathan Vos Post on April 11, 2009 7:40 PM | Permalink | Reply to this

Re: Properties of Structures of Stuff; Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

I don’t see any obvious connection between the two. What do you have in mind?

Posted by: Mike Shulman on April 11, 2009 8:38 PM | Permalink | Reply to this

Re: Properties of Structures of Stuff; Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

A clear default connection between “Structures of one element of Stuff”, “Structures of all my (maybe much bigger than any Set) Stuff”, “Properties of Structures of one element of Stuff”, and “Properties of Structures of all my (maybe much bigger than any Set) Stuff”. With extra attention to what survives forgetful functors and what is Faithful. Or is this already obvious to everyone but me?

Posted by: Jonathan Vos Post on April 11, 2009 10:27 PM | Permalink | Reply to this

Re: Properties of Structures of Stuff; Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Sorry, I still have no idea what you are talking about. (-:

Posted by: Mike Shulman on April 12, 2009 8:00 AM | Permalink | Reply to this

Jeffrey Morton on Categorification and Matter; Re: Properties of Structures of Stuff; Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Mike: this all comes from what I learned in the n-category cafe and things it [pointed to and discussed.

Categorification and Matter Posted by Jeffrey Morton under category theory, philosophical, physics, tqft http://theoreticalatlas.wordpress.com/

Stuff, Structure, and Properties

One aspect of the relationship which I wanted to comment on, one that almost seems like a pun, is the trichotomy which John Baez and Jim Dolan like to use in describing mathematical, um, widgets (I would use the more standard term “objects”, or maybe “structures”, but both of these words have technical meanings in the following) in categorical terms. This is the distinction between “stuff”, “structure”, and “properties”. (More details here and via subsequent links - some of which shows up in my first paper).

http://arxiv.org/abs/math.QA/0601458

Almost any usual mathematical widget can be broken down this way: (1) they consist of some “stuff”, often in the form of some sets; (2) the stuff is equipped with “structure”, often described by some functions; (3) the structure satisfies some “properties”, often expressed as equations.

For example: a group is (1) a set G of elements, equipped with (2) a group operation (expressed as a function m : G x G –> G), and a special identity element (picked out by a function from the one-element set, 1 : * –> G), and an inverse for each element (given by an inverse function inv : G –> G. These satisfy (3) the group axioms, which are some equations involving expressing some properties - associativity, the properties of 1 and inverses.

In this case, the structure live inside the category of sets and functions - but similar things could be said in any other category. For instance, in the category of topological spaces and continuous functions, the same setup gives the definition of a topological group, likewise divided into “stuff” (objects, in this case topological spaces), “structure” (some morphisms), and “properties” (equations between morphisms).

Widgets which live in an n-category of some kind have more of these layers - such a widget will be specified by one or more objects, equipped with specified morphisms and 2-morphisms, satisfying some equations. A monoidal category, for instance, is this kind of widget: it has a category worth of “elements”, equipped with a monoidal operation given as a functor, equipped in turn with specified 2-isomorphisms such as the “associator”, which satisfies some equations such as the Pentagon identity. There are now FOUR levels to specify. I think it was Jim Dolan who came up with the following way of extending the “stuff/structure/properties” terminology (his explanation). http://groups.google.com/group/sci.physics.research/msg/74eb0a6442ecade9

The highest level - equations - always deserves the name “properties”, since they either hold, or don’t (at least, there’s a truth value associated to them - but let’s not worry about multiple-valued logics). By analogy, this suggests the data for our widget given by the n-morphisms in the n-category where it lives should be called “structure”. The (n-1)-morphisms (which are the objects in a 1-category) should be called “stuff”.

For the (n-2), (n-3), and generally k-morphisms, Jim introduces the prefix “eka”, as in “eka-stuff”, which follows Mendeleev’s nomenclature for elements predicted by his form of the periodic table of elements which were heavier than known ones. This nomenclature in turn comes from the Sanskrit “eka”, meaning “one” - the new elements were one level lower on the periodic table.

So specifying a widget in a 2-category involves “eka-stuff/stuff/structure/properties”. This is suggestive, in that it seems as if categorification - adding a new level - is like digging out a new sub-basement beneath a house. First “eka-stuff”, then “eka-eka-stuff”, and so on, to “eka^k-stuff”. Since, in many versions of n-category, given two objects x and y, the totality of morphisms hom(x,y) form an (n-1)-category, this is somewhat correct: there is an (n-1)-categorical structure describing each hom(x,y).

(The periodic-table analogy, I suppose, is meant to imply that the best-understood layer is the layer of equations - which describe properties. This opposes what is probably the more common intuition people have when first encountering higher categories, that we know what “objects” are, but find “higher morphisms” confusing. But when writing things concretely, it’s the highest-level morphisms which look most familiar, like functions.)

A key point here is that “stuff having structure satisfying properties” is a fairly intuitive framework for talking about things. Categorification gives us a more nuanced layering. It may seem odd to speak of “eka-stuff equipped with stuff equipped with structure satisfying properties” (even worse if you want to be consistent, and say “equipped with” instead of “satisfying”). But now the second layer - stuff, refers to 1-morphisms. Here is a layer which has some aspects we associate with “structure”: it describes relations between the eka-stuff (objects). On the other hand, it also has aspects we associate with “stuff” (it can be equipped with its own structure). When would one want something that is on the one hand something like a relational attribute between things (structure), and on the other hand something like an object in its own right (stuff).

One answer: to describe space. As a good Leibnizian, I prefer to think of space relationally: it describes how objects are situated in terms of structural relationships. On the other hand, General Relativity tells us that if we think about space, rather than spacetime, we need to describe it as having dynamics which satisfy some property. From this point of view, space is like material stuff that changes over time, according to some differential equation (classically, at least).

Posted by: Jonathan Vos Post on April 13, 2009 7:01 AM | Permalink | Reply to this

Re: Jeffrey Morton on Categorification and Matter; Re: Properties of Structures of Stuff; Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Sorry, I know about properties, structure, and stuff; I just don’t know what you are proposing that it has to do with gros and petit toposes.

There are some comments about how properties, structure, and stuff are related to classifying toposes in the appendix of this paper. But that doesn’t really seem to be what you are driving at?

Posted by: Mike Shulman on April 13, 2009 9:38 AM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

My impression is that you can always just take your site to be a small full subcategory of TopTop. (If DiffDiff means the category of finite-dimensional connected manifolds, then it is already small.) The only reason I can think of that this would be a problem is if you are interested in some particular very big (but still, of course, small in the technical sense) topological space which is not in your full subcategory—but then given your interest in this space, you should really just have chosen a larger small full subcategory to begin with which includes it. The resulting category of sheaves will not be the same for different choices of the site, but it will share most of the properties we tend to be interested in, so I don’t think there is any reason to worry about precisely what site we have chosen until we need to think about particular spaces. Do you have any problems that this procedure doesn’t solve?

I’m not really sure whether this question has anything to do with the topos having enough points. But I don’t really know enough about topos theory to address that question.

Posted by: Mike Shulman on April 11, 2009 8:25 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Forgive my ignorance, but what is meant by the claim that “It’s only monads having ‘operations’ of potentially arbitrarily large arities, like the monads whose algebras are complete lattices or compact Hausdorff spaces, which don’t fit the Lawvere theory framework.”? Why would arbitrarily large arities present a problem? Cannot one just take the obvious large category (with an object for each arity) to serve as the Lawvere theory?

Posted by: Sridhar Ramesh on April 12, 2009 11:31 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Allowing ‘large’ Lawvere theories might be an interesting thing to study, but it would be a very different subject. Usually when we think of ‘algebraic structure’ we think of a small amount of structure (in the technical sense). If you allow a large amount of structure then you might get, for instance, a proper class of possible structures on a given set. Also, in general, a large Lawvere theory would not generate a monad at all, so free structures would not exist. And depending on your foundations and definitions, it’s less clear whether coproducts and tensor products would continue to exist.

Also, I believe complete lattices could be described by a ‘large’ Lawvere theory, but this is much less clear for compact Hausdorff spaces, since their ‘operations’ are indexed by ultrafilters rather than by subsets. (Hence the scare quotes around ‘operations.’) It might be possible to do something with nets, however. But there’s definitely no a priori reason that all monads could be presented by a ‘large’ Lawvere theory.

Posted by: Mike Shulman on April 13, 2009 9:35 AM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Perhaps I am being confused, but it seems to me straightforward that monads (on Set) and (locally small but with an object for each arity) Lawvere theories are equivalent. Given a monad M on Set, one takes as Lawvere theory L the dual of M’s Kleisli category [which works since the objects of Set are generated as coproducts of 1 of each arity]. Conversely, given a locally small Lawvere theory L whose objects are X^k for arbitrary arities k, we construct a monad on Set which maps a to Hom(X^k, X) [with unit given by projections and multiplication given by “composition”, so to speak]. Extending this correspondence to observe that M-algebras and power-preserving functors from L to Set seems equally as straightforward.

But I’m no expert and that all seems very basic, so I am surely tripping up over something introductory somewhere. Do you have any concrete examples to help illustrate the problem with the above equivalence?

Posted by: Sridhar Ramesh on April 13, 2009 6:37 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

(Sorry, that should of course have been in reply to the above comment (I’m still getting used to how the commenting system here works). Also, the last line of the first paragraph should read “…observe that M-algebras _correspond to_ power-preserving…”.)

Posted by: Sridhar Ramesh on April 13, 2009 6:40 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Argh, also, the third line of the first paragraph should end with “…which maps _k_ to Hom(X^k, X)…”. Looks like I should have previewed better.

Posted by: Sridhar Ramesh on April 13, 2009 6:45 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

I’m no expert either, but I think that you’re OK as long as the Lawvere theory LL is locally small. I’m basing this on Robinson’s paper Variations on algebra, where he says

… a monad without rank [i.e. not preserving κ\kappa-filtered colimits] can be regarded as generating a theory with a proper class of operations and equations… theories arising in this way have only a set of operations of any given arity, and so are dealt with by the theory above [monads \sim algebraic theories] unless they have basic operations of unbounded arity.

He also mentions the fact (which Mike alluded to) that some theories that need operations of unbounded arities (Robinson’s example is complete Boolean algebras) don’t have free algebras in SetSet – that is, the free structures are proper classes, so that there can be no corresponding monad.

I’m really just quoting here; I don’t quite understand it all myself, but I hope this helps.

Posted by: Finn Lawler on April 13, 2009 8:51 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

You all are right and I am wrong; I’m not sure what I was thinking. Monads are completely equivalent to ‘locally small Lawvere theories’ in the way that Sridhar described. So you can think of an arbitrary monad that way, and indeed it can be conceptually helpful to do so—but the point is rather that all the good properties of small Lawvere theories, such as those listed above, generally don’t carry over to their large brethren (i.e. monads). The case of complete Boolean algebras, for instance, is one where a system of ‘generators and relations’ for a monad fails to actually present one.

Posted by: Mike Shulman on April 14, 2009 1:32 AM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

That sounds right – it seems the point is that it’s not that you can’t have a large Lawvere theory, it’s that restricting to the finitary or κ\kappa-presentable case gives you a much nicer meta-theory. For example, you can often guarantee the existence of initial and free algebras.

Also, I think Power is right that Lawvere theories are the right way to do universal algebra using categories, especially in computer science. He and Hyland have been arguing for some years now that computer scientists should be using them for structuring semantics in the way that Moggi used monads: in particular, the ‘smallness’ (boundedness-by-a-regular-cardinal) stipulation seems to isolate the theories/monads that genuinely correspond to side-effects in programming. Contrast the ‘continuation’ monad A(A2)2A\mapsto (A\to 2)\to 2, which doesn’t have rank: continuation-passing is not really a side-effect, or so the conventional wisdom has it.

Posted by: Finn Lawler on April 14, 2009 5:56 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

That’s certainly an interesting point of view. On the other hand, continuation-passing is important, even if it is not a ‘side effect.’

Also, I don’t see how Lawvere theories could be used in a programming language with the same elegance and power that monads have in, say, Haskell. Have Power and Hyland addressed that?

Posted by: Mike Shulman on April 19, 2009 3:31 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

[Apologies for the delayed reply: I think your comment fell off the end of the RSS feed before I saw it.]

I don’t think Hyland and Power intend Lawvere theories to be used inside a programming language, in the way monads are in Haskell. I think they’re just considering the semantics of languages.

One slight embarassment with monads in Haskell is that they don’t compose, so combining two monads into one is non-trivial and messy, and the same problem crops up in semantics. Lawvere theories, on the other hand, have natural notions of sum and product, which is one reason H&P argue for them. It would be nice to have support for something like this (sum and product of effects) in a programming language, but I’m not sure what that would look like.

Posted by: Finn Lawler on May 6, 2009 9:16 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

I wouldn’t call it an embarassment that monads don’t compose; it’s just a fact that the composite of monads isn’t a monad. It may be a little messy to specify how to put monads together, but this just reflects the fact that you actually do need to specify how to put two monads together if you want to get another one; it doesn’t happen automatically. Sum and product of effects are interesting ideas, but seem probably quite different from the way that monads generally are put together in haskell.

Posted by: Mike Shulman on May 7, 2009 7:19 PM | Permalink | Reply to this
Read the post Kamnitzer on Categorifying Tangle Invariants
Weblog: The n-Category Café
Excerpt: A brief summary of a talk by Joel Kamnitzer at the workshop on Categorification and Geometrisation from Representation Theory.
Tracked: April 14, 2009 1:42 PM

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

That’s a great overview of the conference, Mike. And thanks for the type theory entry.

I wonder if something I don’t get fits in with what you wrote there. It’s the idea, apparently described in D1 of The Elephant (unfortunately, inaccessible for me), of generating a syntactic category 𝒞 𝕋\mathcal{C}_{\mathbb{T}} from a many-sorted first-order 𝕋\mathbb{T}.

Objects are alpha-equivalence classes of formulas-in-context, and arrows are equivalence classes of formulas-in-context satisfying various conditions. The result is a Boolean coherent category.

Posted by: David Corfield on April 16, 2009 12:02 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

I’m assuming you are referring to the construction which takes objects as definable predicates, and arrows as definable provably functional relations on the extensions of those predicates, all modulo provable equivalence? [Essentially, augmenting the starting theory with “comprehension” and “definition by description”, so to speak, and then taking the resulting category of terms, inheriting whatever logical structure the underlying theory has]

You describe this as something you don’t get, so I am curious. What is it about this that you don’t “get” (i.e., what questions about this do you have?)?

Posted by: Sridhar Ramesh on April 16, 2009 8:30 PM | Permalink | Reply to this

Re: Report on 88th Peripatetic Seminar on Sheaves and Logic

Let’s see what we have. My only access is Forssell’s thesis mentioned here. On p. 34 he writes that the syntactic category associated to a coherent theory 𝕋\mathbb{T}, 𝒞 𝕋\mathcal{C}_{\mathbb{T}}, has as objects alpha-equivalence classes of formulas-in-context, [x|ϕ][\vec{x}| \phi] of 𝕋\mathbb{T}.

An arrow between objects [x|ϕ][\vec{x}|\phi] and [y|ψ][\vec{y}|\psi] is a 𝕋\mathbb{T}-provable equivalence class of formulas-in-context [x,y|σ][\vec{x}, \vec{y}| \sigma] such that the following sequents are in 𝕋\mathbb{T}:

  • σ x,yϕψ\sigma \vdash_{\vec{x}, \vec{y}} \phi \wedge \psi
  • ϕ xy.σ\phi \vdash_{\vec{x}} \exists \vec{y}.\sigma
  • σσ[z/y] x,y,zy=z.\sigma \wedge \sigma[\vec{z}/\vec{y}] \vdash_{\vec{x}, \vec{y}, \vec{z}} \vec{y} = \vec{z}.

So your comment is telling me that these conditions are there to specify

definable provably functional relations on the extensions of those predicates.

OK, that makes sense.

Posted by: David Corfield on April 17, 2009 11:12 AM | Permalink | Reply to this
Read the post In Search of Terminal Coalgebras
Weblog: The n-Category Café
Excerpt: Trying to understand a talk on terminal coalgebras
Tracked: May 8, 2009 10:14 AM

Post a New Comment