Algebraic theories and commutativity in a sheaf topos

TL;DR

This paper develops a generalized framework for algebraic theories within sheaf topoi, establishing model categories as stacks and exploring their monoidal structures, with applications to linear spaces and Lebesgue integration.

Contribution

It introduces a notion of $ au$-theories over sites, constructs model stacks, and shows how commutative theories induce monoidal structures, extending Lawvere's theories to sheaf topoi.

Findings

Models form stacks over $ ext{ extbf{E}}$

Existence of free-forget adjunctions for models

Monoidal structures for commutative theories

Abstract

For any site of definition $\mathcal C$ of a Grothendieck topos $\mathcal E$, we define a notion of a $\mathcal C$-ary Lawvere theory $\tau: \mathscr C \to \mathscr T$ whose category of models is a stack over $\mathcal E$. Our definitions coincide with Lawvere's finitary theories when $\mathcal C=\aleph_0$ and $\mathcal E = \operatorname{\mathbf {Set}}$. We construct a fibered category $\operatorname{\mathbf {Mod}}^{\mathscr T}$ of models as a stack over $\mathcal E$ and prove that it is $\mathcal E$-complete and $\mathcal E$-cocomplete. We show that there is a free-forget adjunction $F \dashv U: \operatorname{\mathbf {Mod}}^{\mathscr T} \rightleftarrows \mathscr E$. If $\tau$ is a commutative theory in a certain sense, then we obtain a ``locally monoidal closed'' structure on the category of models, which enhances the free-forget adjunction to an adjunction of symmetric monoidal $\mathcal E$-categories. Our results give a general recipe for constructing a monoidal $\mathcal E$-cosmos in which one can do enriched $\mathcal E$-category theory. As an application, we describe a convenient category of linear spaces generated by the theory of Lebesgue integration.