September 28, 2023
Lectures on Applied Category Theory
Posted by John Baez
Want to learn applied category theory? You can now read my lectures here:
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. 😢
September 23, 2023
The Moduli Space of Acute Triangles
Posted by John Baez
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.
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 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!
September 17, 2023
Counting Algebraic Structures
Posted by John Baez
The number of groups with elements goes like this, starting with :
0, 1, 1, 1, 2, 1, 2, 1, 5, …
The number of semigroups with 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 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 for an arbitrary endofunctor .
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 with a finite set of relations on , is essentially a database in the sense of good old SQL tables, and a logic formula with free variables is understood as a query to the database that selects all -tuples of that satisfy the formula .
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 -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 is a way to speak about the “location” of a process taking place in , but without referring to points, space, or distance. Under mild conditions on , its set of central idempotents can be viewed as a sort of “topological space internal to ,” which lets us use some tools and intuition from topology while working in .
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 .
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 is a separable extension of if and only if it’s a separable algebra over .
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 ‘’ thingies you see in calculus and differential geometry. They’re called Kähler differentials, and I introduced them last time.