The n-Category Café

Want to learn applied category theory? You can now read my lectures here:

• Lectures on applied category theory

There are a lot, but each one is bite-sized and basically covers just one idea. They’re self-contained, but you can also read them along with Fong and Spivak’s free book to get two outlooks on the same material:

• Brendan Fong and David Spivak, Seven Sketches in Compositionality: An Invitation to Applied Category Theory.

Huge thanks go to Simon Burton for making my lectures into nice web pages! But they still need work. If you see problems, please let me know.

Here’s one problem: I need to include more of my ‘Puzzles’ in these lectures. None of the links to puzzles work. Students in the original course also wrote up answers to all of these puzzles, and to many of Fong and Spivak’s exercises. But it would take quite a bit of work to put all those into webpage form, so I can’t promise to do that. 😢

I wrote a little article explaining the concept of ‘moduli space’ through an example. It’s due October 1st so I’d really appreciate it if you folks could take a look and see if it’s clear enough. It’s really short, and it’s written for people who know some math, but not necessarily anything about moduli spaces.

I’m in Regensburg this week attending a workshop on Interactions of Proof Assistants and Mathematics. One of the lecture series is being given by John Harrison, a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services, and a lead developer of the HOL Light interactive theorem prover. He just told us about a very cool construction of the non-negative real numbers as sequences of natural numbers satisfying a property he calls “near multiplicativity”. In particular, the integers and the rational numbers aren’t needed at all! This is how the reals are constructed in HOL Light and is described in more detail in a book he wrote entitled Theorem Proving with the Real Numbers.

Edit: as the commenters note, these are also known as the Eudoxus reals and were apparently discovered by our very own Stephen Schanuel and disseminated by Ross Street. Thanks for pointing me to the history of this construction!

The number of groups with $n$ elements goes like this, starting with $n = 0$:

0, 1, 1, 1, 2, 1, 2, 1, 5, …

The number of semigroups with $n$ elements goes like this:

1, 1, 5, 24, 188, 1915, 28634, 1627672, 3684030417, 105978177936292, …

Here I’m counting isomorphic guys as the same.

But how much do we know about such sequences in general? For example, is there any sort of algebraic gadget where the number of gadgets with $n$ elements goes like this:

1, 1, 2, 1, 1, 1, 1, 1, … ?

guest post by Keri D’Angelo, Johanna Maria Kirss and Matina Najafi and Wojtek Rozowski

Long ago, coalgebras of all kinds lived together: deterministic and nondeterministic automata, transition systems of the labelled and probabilistic varieties, finite and infinite streams, and any other arrows $\alpha: X\to F X$ for an arbitrary endofunctor $F:\mathcal{C}\to\mathcal{C}$.

guest post by Elena Dimitriadis, Richie Yeung, Tyler Hanks, and Zhixuan Yang

In the Part 1 of this post, we saw how logical equivalences of first-order logic (FOL) can be characterised by a combinatory game, but there are still a few unsatisfactory aspects of the formulation of EF games in Part 1:

1. The game was formulated in a slightly informal way, delegating the precise meaning of “turns”, “moves”, “wins” to our common sense.

2. There are variants of the EF game that characterise logical equivalences for other logics, but these closely related games are defined ad hoc rather than as instances of one mathematical framework.

3. We have confined ourselves entirely to the classical semantics of FOL in the category of sets, rather than general categorical semantics.

So you, a patron of the n-Category Café, must be thinking that category theory is perfect for addressing these problems! This is exactly what we are gonna talk about today—the framework of game comonads that was introduced by Abramsky, Dawar and Wang (2017) and Abramsky and Shah (2018).

(We will not address the third point above in this post though, but hopefully the reader will agree that what we talk about below is a useful first step towards model comparison games for general categorical logic.)

guest post by Elena Dimitriadis, Richie Yeung, Tyler Hanks, and Zhixuan Yang

Finite model theory (Libkin 2004) studies finite models of logics. Its main motivation comes from computer science: a finite relational structure, i.e. a finite set $A$ with a finite set of relations on $A$, is essentially a database in the sense of good old SQL tables, and a logic formula $\varphi$ with $n$ free variables is understood as a query to the database that selects all $n$-tuples of $A$ that satisfy the formula $\varphi$.

guest post by Paige Frederick, Durgesh Kumar and Fabian Wiesner

Concurrency is the process of running different processes in non-sequential order while not affecting the desired output. In practice, how processes act together is designed by humans and thus subject to potential errors. These errors motivate the formalization of concurrency, which prevents errors in the design of concurrent processes.

A very general approach to this is the paper The Logic of Message Passing [CP07] by Cockett and Pastro from 2007. In this blog post for the Applied Category Theory Adjoint School 2023 we present concurrency, their definition of linear actegories and motivate how the former can be formalized by the latter.

guest post by Brandon Baylor and Isaiah B. Hilsenrath

In the study of categories with two binary operations, one usually assumes a distributivity condition (e.g., how multiplication distributes over addition). However, today we’ll introduce a different type of structure, defined by Cockett and Seely, known as a linearly distributive category or LDC (originally called a weakly distributive category). See:

• J. R. B. Cockett and R. A. G. Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114(2):133-173, 1997.

LDCs are categories with two tensor products linked by coherent linear (or weak) distributors. The significance of this theoretical development stems from many situations in logic, theoretical computer science, and category theory where tensor products play a key role. We have been particularly motivated to study LDCs from the setting of categorical quantum mechanics, where the application of LDCs supports a novel framework that allows the study of quantum processes of arbitrary dimensions (compared to well-known approaches that are limited to studying finite dimensions), so in addition to defining LDCs, we’ll use $\ast$-autonomous categories to briefly touch upon the advantages LDCs offer in the context of quantum mechanics.

guest post by Ariel Rosenfield and Ariadne Si Suo

One can view a monoidal category as a collection of resources (objects) and processes for transforming resources (morphisms). A central idempotent in a monoidal category $(\mathbf{C}, \otimes, I)$ is a way to speak about the “location” of a process taking place in $\mathbf{C}$, but without referring to points, space, or distance. Under mild conditions on $\mathbf{C}$, its set $ZI(\mathbf{C})$ of central idempotents can be viewed as a sort of “topological space internal to $\mathbf{C}$,” which lets us use some tools and intuition from topology while working in $\mathbf{C}$.

Our Adjoint School group spent a lot of time the past few months with this paper by Rui Barbosa and Chris Heunen, which outlines a particularly cool application of this idea, namely the representation of “nice enough” monoidal categories (those satisfying the aforementioned mild conditions) as the global sections of certain sheaves. In this post, we’ll take a close look at central idempotents and two related notions, namely the restriction and support of morphisms in $\mathbf{C}$.

It’s Hoàng Xuân Sính’s 90th birthday today! Here she is in front of Grothendieck in 1967:

He taught algebraic geometry in the countryside in Vietnam while Hanoi was being bombed, and she took notes. After he left she did her thesis with him by correspondence! When the war ended, she went to Paris to defend her thesis and get her Ph.D. Then she returned to Hanoi and started the first private university in Vietnam.

A while ago Hà Huy Khoái, director of the Mathematics Institute at the Vietnam Academy of Science and Technology, asked me to write an essay about Hoàng Xuân Sính’s thesis for a book in honor of her birthday. He didn’t tell me it was going to be a printing of her thesis. In all these years, her thesis had never been published!

guest post by Clémence Chanavat and Luke Morris

Let’s motivate this blog post by first formalizing what a resource theory is. Coecke et al. represent a resource theory in “A mathematical theory of resources” as a symmetric monoidal category (SMC), which is a familiar construction in applied category theory. Elegantly, each of the concepts used in defining a symmetric monoidal category has a simple physical intuition:

• Objects are resources
• Morphisms transform resources to other resources
• Composition is sequential transformation
• Tensoring is parallel transformation
• The unit is the “void resource”

Using the usual string diagram approach, we get diagrams representing resource transformations for free! We thus have a very expressive visual language for expressing resource transformations, and a familiar ACT formalization.

The word ‘separable’ is annoying at first. In Galois theory we learn that ‘separable field extensions’ are the nice ones to work with, though their definition seems dry and technical. There’s also a concept of ‘separable algebra’. This is defined in a different way — and not every separable field extension is a separable algebra! So what’s going on?

Today I’ll remind you of these two concepts and show you why a finite-dimensional extension of a field $k$ is a separable extension of $k$ if and only if it’s a separable algebra over $k$.

I got my arguments for this from Tom Leinster and Qing Liu. Their arguments are nice because they use differential geometry. More precisely, they use an algebraic approach to those ‘$d x$’ thingies you see in calculus and differential geometry. They’re called Kähler differentials, and I introduced them last time.