The n-Category Café

The ‘geometric McKay correspondence’, actually discovered by Patrick du Val in 1934, is a wonderful relation between the Platonic solids and the ADE Dynkin diagrams. In particular, it sets up a connection between two of my favorite things, the icosahedron:

and the $\mathrm{E}_8$ Dynkin diagram:

When I recently gave a talk on this topic, I realized I didn’t understand it as well as I’d like. Since then I’ve been making progress with the help of this book:

• Alexander Kirillov Jr., Quiver Representations and Quiver Varieties, AMS, Providence, Rhode Island, 2016.

I now think I glimpse a way forward to a very concrete and vivid understanding of the relation between the icosahedron and E₈. It’s really just a matter of taking the ideas in this book and working them out concretely in this case. But it takes some thought, at least for me. I’d like to enlist your help.

guest post by Mike Stay

Last year, my son’s math teacher introduced the kids to the concept of a function. One of the major points of confusion in the class was the idea that it didn’t matter whether he wrote $f(x) = x^2$ or $f(y) = y^2$, but it did matter whether he wrote $f(x) = x y$ or $f(x) = x z$. The function declaration binds some of the variables appearing on the right to the ones appearing on the left; the ones that don’t appear on the left are “free”. In a few years when he takes calculus, my son will learn about the quantifiers “for all” and “there exists” in the “epsilon-delta” definition of limit; quantifiers also bind variables in expressions.

Reasoning formally about languages with binders is hard:

“The problem of representing and reasoning about inductively-defined structures with binders is central to the PoplMark challenges. Representing binders has been recognized as crucial by the theorem proving community, and many different solutions to this problem have been proposed. In our (still limited) experience, none emerge as clear winners.” – Aydemir, Bohannon, Fairbairn, Foster, Pierce, Sewell, Vytiniotis, Washburn, Weirich, and Zdancewic, Mechanized metatheory for the masses: The PoplMark challenge. (2005)

The paper quoted above reviews around a dozen approaches in section 2.3, and takes pains to point out that their review is incomplete. However, recently Andrew Pitts and his students (particularly Murdoch Gabbay) developed the notion of a nominal set (introductory slides, book) that has largely solved this problem. Bengston and Barrow use a nominal datatype package in Isabell/HOL to formalize $\pi$-calculus, and Clouston defined nominal Lawvere theories. It’s my impression that pretty much everyone now agrees that using nominal sets to formally model binders is the way forward.

Sometimes, though, it’s useful to look backwards; old techniques can lead to new ways of looking at a problem. The earliest approach to the problem of formally modeling bound variables was to eliminate them.

guest post by Mike Stay

Programs are an expression of programmer intent. We want the computer to do something for us, so we need to tell it what to do. We make mistakes, though, so we want to be able to check somehow that the program will do what we want. The idea of semantics for a programming language is that we assign some meaning to programs in such a way that we can reason about the behavior of a program. There are two main approaches to this: denotational semantics and operational semantics. I’ll discuss both below, but the post will focus for the most part on operational semantics.

There’s a long history of using 2-categories and related structures for term rewriting and operational semantics, but Greg Meredith and I are particularly fond of an approach using multisorted Lawvere theories enriched over the category of reflexive directed graphs, which we call Gph. Such enriched Lawvere theories are equal in power to, for instance, Sassone and Sobociński’s reactive systems, but in my opinion they have a cleaner categorical presentation. We wrote a paper on them:

• Representing operational semantics with enriched Lawvere theories.

Here I’ll just sketch the basic ideas.

One of the observations that launched homotopy type theory is that the rule of identity-elimination in Martin-Löf’s identity types automatically generates the structure of an $\infty$-groupoid. In this way, homotopy type theory can be viewed as a “synthetic theory of $\infty$-groupoids.”

It is natural to ask whether there is a similar directed type theory that describes a “synthetic theory of $(\infty,1)$-categories” (or even higher categories). Interpreting types directly as (higher) categories runs into various problems, such as the fact that not all maps between categories are exponentiable (so that not all $\prod$-types exist), and that there are numerous different kinds of “fibrations” given the various possible functorialities and dimensions of categories appearing as fibers. The 2-dimensional directed type theory of Licata and Harper has semantics in 1-categories, with a syntax that distinguishes between co- and contra-variant dependencies; but since the 1-categorical structure is “put in by hand”, it’s not especially synthetic and doesn’t generalize well to higher categories.

An alternative approach was independently suggested by Mike and by Joyal, motivated by the model of homotopy type theory in the category of Reedy fibrant simplicial spaces, which contains as a full subcategory the $\infty$-cosmos of complete Segal spaces, which we call Rezk spaces. It is not possible to model ordinary homotopy type theory directly in the Rezk model structure, which is not right proper, but we can model it in the Reedy model structure and then identify internally some “types with composition,” which correspond to Segal spaces, and “types with composition and univalence,” which correspond to the Rezk spaces.

Almost five years later, we are finally developing this approach in more detail. In a new paper now available on the arXiv, Mike and I give definitions of Segal and Rezk types motivated by these semantics, and demonstrate that these simple definitions suffice to develop the synthetic theory of $(\infty,1)$-categories. So far this includes functors, natural transformations, co- and contravariant type families with discrete fibers ($\infty$-groupoids), the Yoneda lemma (including a “dependent” Yoneda lemma that looks like “directed identity-elimination”), and the theory of coherent adjunctions.

Guest post by José Siqueira

We began our journey in the second Kan Extension Seminar with a discussion of the classical concept of Lawvere theory , facilitated by Evangelia. Together with the concept of a model, this technology allows one to encapsulate the behaviour of algebraic structures defined by collections of $n$-ary operations subject to axioms (such as the ever-popular groups and rings) in a functorial setting, with the added flexibility of easily transferring such structures to arbitrary underlying categories $\mathcal{C}$ with finite products (rather than sticking with $\mathbf{Set}$), naturally leading to important notions such as that of a Lie group.

Throughout the seminar, many features of Lawvere theories and connections to other concepts were unearthed and natural questions were addressed — notably for today’s post, we have established a correspondence between Lawvere theories and finitary monads in $\mathbf{Set}$ and discussed the notion of operad, how things go in the enriched context and what changes if you tweak the definitions to allow for more general kinds of limit. We now conclude this iteration of the seminar by bringing to the table “Monads with arities and their associated theories”, by Clemens Berger, Paul-André Melliès and Mark Weber, which answers the (perhaps last) definitional “what-if”: what goes on if you allow for operations of more general arities.

At this point I would like to thank Alexander Campbell, Brendan Fong and Emily Riehl for the amazing organization and support of this seminar, as well as my fellow colleagues, whose posts, presentations and comments drafted a more user-friendly map to traverse this subject.

Guest post by Daniel Cicala

The Kan Extension Seminar II continues with a discussion of the paper Notions of Lawvere Theory by Stephen Lack and Jirí Rosický.

In his landmark thesis, William Lawvere introduced a method to the study of universal algebra that was vastly more abstract than those previously used. This method actually turns certain mathematical stuff, structure, and properties into a mathematical object! This is achieved with a Lawvere theory: a bijective-on-objects product preserving functor $T \colon \aleph^{\text{op}}_0 \to \mathbf{L}$ where $\aleph_0$ is a skeleton of the category $\mathbf{FinSet}$ and $\mathbf{L}$ is a category with finite products. The analogy between algebraic gadgets and Lawvere theories reads as: stuff, structure, and properties correspond respectively to 1, morphisms, and commuting diagrams.

To get an actual instance, or a model, of an algebraic gadget from a Lawvere theory, we take a product preserving functor $m \colon \mathbf{T} \to \mathbf{Set}$. A model picks out a set $m(1)$ and $n$-ary operations $m(f) \colon m(1)^n \to m(1)$ for every $T$-morphism $f \colon n \to 1$.

To read more about classical Lawvere theories, you can read Evangelia Aleiferi’s discussion of Hyland and Power’s paper on the topic.

With this elegant perspective on universal algebra, we do what mathematicians are wont to do: generalize it. However, there is much to consider undertaking such a project. Firstly, what elements of the theory ought to be generalized? Lack and Rosický provide a clear answer to this question. They generalize along the following three tracks:

• consider a class of limits besides finite products,

• replace the base category $\mathbf{Set}$ with some other suitable category, and

• enrich everything.

Another important consideration is to determine exactly how far to generalize. Why not just go as far as possible? Here are two reasons. First, there are a number of results in this paper that stand up to further generalization if one doesn’t care about constructibility. A second limiting factor of generalization is that one should ensure that central properties still hold. In Notions of Lawvere Theory, the properties lifted from classical Lawvere theories are

• the correspondence between Lawvere theories and monads,

• that algebraic functors have left adjoints, and

• models form reflective subcategories of certain functor categories.

Before starting the discussion of the paper, I would like to take a moment to thank Alexander, Brendan and Emily for running this seminar. I have truly learned a lot and have enjoyed wonderful conversations with everyone involved.

I’ve just finished teaching a seminar course officially called “Functional Equations”, but really more about the concepts of entropy and diversity.

I’m grateful to the participants — from many parts of mathematics, biology and physics, at levels from undergraduate to professor — who kept coming and contributing, week after week. It was lots of fun, and I learned a great deal.

This post collects together all the material in one place. First, the notes:

• Tom Leinster, Functional Equations. Rough and ready course notes, University of Edinburgh, 2017.

Now, the posts I wrote every week:

• I. Cauchy’s equation
• II. Shannon entropy
• III. Explaining relative entropy
• IV. A simple characterization of relative entropy
• V. Expected surprise
• VI. Using probability theory to solve functional equations
• VII. The $p$-norms
• VIII. Measuring biodiversity
• IX. Entropy on a metric space
• X. Value
• XI. The diversity of a metacommunity

The eleventh and final installment of the functional equations course can be described in two ways:

• From one perspective, I talked about conditional entropy, mutual information, and a very appealing analogy between these concepts and the most basic primary-school Venn diagrams.

• From another, it was about diversity across a metacommunity, that is, an ecological community divided into smaller communities (e.g. geographical sites).

The notes begin on page 44 here.

Guest post by Pierre Cagne

The Kan Extension Seminar II continues with a third consecutive of Kelly, entitled On clubs and data-type constructors. It deals with the notion of club, first introduced by Kelly as an attempt to encode theories of categories with structure involving some kind of coherence issues. Astonishing enough, there is no mention of operads whatsoever in this article. (To be fair, there is a mention of “those Lawvere theories with only associativity axioms”…) Is it because the notion of club was developed in several stages at various time periods, making operads less identifiable among this work? Or does Kelly judge irrelevant the link between the two notions? I am not sure, but anyway I think it is quite interesting to read this article in the light of what we now know about operads.

Before starting with the mathematical content, I would like to thank Alexander, Brendan and Emily for organizing this online seminar. It is a great opportunity to take a deeper look at seminal papers that would have been hard to explore all by oneself. On that note, I am also very grateful for the rich discussions we have with my fellow participants.

What is the value of the whole in terms of the values of the parts?

More specifically, given a finite set whose elements have assigned “values” $v_1, \ldots, v_n$ and assigned “sizes” $p_1, \ldots, p_n$ (normalized to sum to $1$), how can we assign a value $\sigma(\mathbf{p}, \mathbf{v})$ to the set in a coherent way?

This seems like a very general question. But in fact, just a few sensible requirements on the function $\sigma$ are enough to pin it down almost uniquely. And the answer turns out to be closely connected to existing mathematical concepts that you probably already know.

The American Mathematical Society is having a meeting here at U. C. Riverside during the weekend of November 4th and 5th, 2017. I’m organizing a session on Applied Category Theory, and I’m looking for people to give talks.

Yesterday’s functional equations class can be described in two ways:

From a mathematical point of view, I gave a definition of the entropy of a probability distribution on a metric space. The high point was a newish maximum entropy theorem (joint work with Mark Meckes).

From a biological point of view, it was all about measuring the diversity of a community in a way that factors in the varying similarity between species. This approach is well-adapted to situations where there’s no clear division into “species” — for instance, communities of microbes. It also addresses a point made yesterday on this blog. All this is based on joint work with Christina Cobbold.

You can read the notes from yesterday’s class on pages 35–38 here.

Toposes come in two varieties: “Grothendieck” and “elementary”. A Grothendieck topos is the category of sheaves of sets on some site. An elementary topos is a cartesian closed category with finite limits and a subobject classifier. Though these definitions seem quite different, they are very closely related: every Grothendieck topos is an elementary topos, while elementary toposes (especially when considered “over a fixed base”) behave very much like Grothendieck ones.

All the fervor about $(\infty,1)$-toposes nowadays has centered on Grothendieck ones: $(\infty,1)$-categories of $\infty$-sheaves of $\infty$-groupoids on $(\infty,1)$-sites. (Technically, this is only true if we use a perhaps-excessively-general notion of “site”, but it’s the right idea.) However, it’s quite natural to speculate about a corresponding notion of elementary $(\infty,1)$-topos. Because an elementary 1-topos is essentially “a category whose internal logic is intuitionistic higher-order type theory”, it’s natural to try to define an elementary $(\infty,1)$-topos to be an $(\infty,1)$-category whose “internal logic” is, or at least should be, a kind of homotopy type theory. However, even laying aside the unresolved questions involved in the “internal logic” of $(\infty,1)$-categories, it’s never been entirely clear to me exactly what “kind” of homotopy type theory we should use here.

Until now, that is. I propose the following definition: an elementary (∞,1)-topos is an $(\infty,1)$-category such that

• It has finite limits and colimits (in the $\infty$-sense, i.e. homotopy limits and colimits).
• It is locally cartesian closed.
• It has a subobject classifier, i.e. a map $\top:1\to \Omega$ such that for any $X$ the hom-$\infty$-groupoid $Hom(X,\Omega)$ is equivalent, by pullback of $\top$, to the $\infty$-groupoid of subobjects of $X$ (which is equivalent to a discrete set). Here a “subobject” is a map $S\to X$ such that each $\infty$-functor $Hom(Z,S) \to Hom(Z,X)$ is fully faithful.
• For any morphism $f:Y\to X$, there exists an object classifier $p:V\to U$ that classifies $f$ (i.e. $f$ is a pullback of $p$) and such that the collection of morphisms it classifies (i.e. the pullbacks of $p$) is closed under composition, finite fiberwise limits and colimits, and dependent products. Here $p:V\to U$ is an “object classifier” if for any $X$, pullback of $p$ yields a fully faithful functor from $Hom(X,U)$ to the core (the maximal sub-$\infty$-groupoid) of the slice $(\infty,1)$-category over $X$.

Guest post by David Jaz Myers

The Kan Extension Seminar continues with Kelly’s Structures defined by limits in the enriched context, I, or as I like to call it, Presenting categories whose objects are glued together out of finite shapes. This paper hit the presses in 1982 and represented both a condensation and generalization of the theory of locally finitely presentable categories. Kelly achieved both the condensing and the generalizing through his use of weighted (or, as he calls them, indexed) limits and colimits. The resulting theory is slick and highly categorical, but very dense. So, in this post, we’re going to button down a bit and skim over a few details so that we can focus on the story and the powerful results which sustain it, rather than the technicalities. I will label the propositions by where they appear in Kelly’s paper, so that you can find the technicalities if you would like.

At first, it will seem like this post is a radical departure from the previous seminar posts. But as we go on, we’ll see that gluing together finite shapes has a lot to do with the categorical approach to algebra that Evangelia wrote about in the post that kicked off our seminar.

Before I start, I’d like to thank Emily, Alexander, and Brendan for organizing this lovely seminar and inviting me to participate. I’d also like to thank my fellow students for their insight and conversation.

Guest post by David Jaz Myers

What are weighted limits and colimits? They’re great, that’s what!

In this post, we prepare for the next part of the Kan Extension Seminar by learning a bit about enrichment and weighted limits and colimits. I’ll also describe the “$\mathcal{V}\,$ point of view” that I’ll be adopting for the next post.