Monads and theories

TL;DR

This paper develops a general framework connecting monads and theories in enriched categories, extending known correspondences and introducing new ones, including applications to weak omega-groupoids.

Contribution

It introduces $ ext{A}$-theories and $ ext{A}$-nervous monads, establishing a broad, almost complete correspondence extending previous work and capturing new structures like globular theories.

Findings

Established an adjoint pair between monads and $ ext{A}$-pretheories.

Characterized $ ext{A}$-nervous monads as fixpoints of the adjunction.

Extended monad--theory correspondences to new contexts, including weak $ ext{omega}$-groupoids.

Abstract

Given a locally presentable enriched category $\mathcal{E}$ together with a small dense full subcategory $\mathcal A$ of arities, we study the relationship between monads on $\mathcal E$ and identity-on-objects functors out of $\mathcal A$, which we call $\mathcal A$-pretheories. We show that the natural constructions relating these two kinds of structure form an adjoint pair. The fixpoints of the adjunction are characterised as the $\mathcal A$-nervous monads---those for which the conclusions of Weber's nerve theorem hold---and the $\mathcal A$-theories, which we introduce here. The resulting equivalence between $\mathcal A$-nervous monads and $\mathcal A$-theories is best possible in a precise sense, and extends almost all previously known monad--theory correspondences. It also establishes some completely new correspondences, including one which captures the globular theories defining Grothendieck weak $\omega$-groupoids. Besides establishing our general correspondence and illustrating its reach, we study good properties of $\mathcal A$-nervous monads and $\mathcal A$-theories that allow us to recognise and construct them with ease. We also compare them with the monads with arities and theories with arities introduced and studied by Berger, Melli\`es and Weber.