## September 22, 2023

### Constructing the real numbers as nearly multiplicative sequences

#### Posted by Emily Riehl

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 his 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.

## September 17, 2023

### Counting Algebraic Structures

#### Posted by John Baez

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, … ?

## September 12, 2023

### Coalgebraic Behavioural Metrics: Part 1

#### Posted by Emily Riehl

*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}$.

## September 11, 2023

### Finite Model Theory and Game Comonads: Part 2

#### Posted by Emily Riehl

*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:

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

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.

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.)

## September 8, 2023

### Finite Model Theory and Game Comonads: Part 1

#### Posted by Emily Riehl

*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$.

## September 7, 2023

### Linear Actegories

#### Posted by Emily Riehl

*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.

## September 6, 2023

### An Introduction to Linearly Distributive Categories

#### Posted by Emily Riehl

*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.

## September 5, 2023

### A Notion of ‘Location’ for Processes in Monoidal Categories

#### Posted by Emily Riehl

*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}$.

### Hoàng Xuân Sính’s Birthday

#### Posted by John Baez

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!

## September 4, 2023

### Concurrent Process Histories and Resource Transducers

#### Posted by Emily Riehl

*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.

## September 1, 2023

### Grothendieck–Galois–Brauer Theory (Part 4)

#### Posted by John Baez

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.