\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{algebraic theory} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{algebra}{}\paragraph*{{Algebra}}\label{algebra} [[!include higher algebra - contents]] \hypertarget{algebraic_theories}{}\section*{{Algebraic theories}}\label{algebraic_theories} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{categorical_formulation}{Categorical formulation}\dotfill \pageref*{categorical_formulation} \linebreak \noindent\hyperlink{basic_intuitions}{Basic Intuitions}\dotfill \pageref*{basic_intuitions} \linebreak \noindent\hyperlink{extensions}{Extensions}\dotfill \pageref*{extensions} \linebreak \noindent\hyperlink{infinitary_operations}{Infinitary operations}\dotfill \pageref*{infinitary_operations} \linebreak \noindent\hyperlink{multisorted_operations}{Multi-sorted operations}\dotfill \pageref*{multisorted_operations} \linebreak \noindent\hyperlink{generalized_algebraic_theories}{Generalized Algebraic Theories}\dotfill \pageref*{generalized_algebraic_theories} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{variations}{Variations}\dotfill \pageref*{variations} \linebreak \noindent\hyperlink{essentially_algebraic_theories}{Essentially algebraic theories}\dotfill \pageref*{essentially_algebraic_theories} \linebreak \noindent\hyperlink{multisorted_algebraic_theories}{Multisorted algebraic theories}\dotfill \pageref*{multisorted_algebraic_theories} \linebreak \noindent\hyperlink{commutative_theories}{Commutative theories}\dotfill \pageref*{commutative_theories} \linebreak \noindent\hyperlink{RelationToMonads}{Relation to monads}\dotfill \pageref*{RelationToMonads} \linebreak \noindent\hyperlink{the_monad_of_a_locally_small_lawvere_theory}{The monad of a locally small Lawvere theory}\dotfill \pageref*{the_monad_of_a_locally_small_lawvere_theory} \linebreak \noindent\hyperlink{large_lawvere_theory_of_a_monad}{Large Lawvere theory of a monad}\dotfill \pageref*{large_lawvere_theory_of_a_monad} \linebreak \noindent\hyperlink{algebras_and_models}{Algebras and models}\dotfill \pageref*{algebras_and_models} \linebreak \noindent\hyperlink{metaphor}{Metaphor}\dotfill \pageref*{metaphor} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} An \emph{algebraic [[theory]]} is a concept in [[universal algebra]] that describes a specific type of algebraic gadget, such as [[group|groups]] or [[ring|rings]]. An individual group or ring is a \emph{model} of the appropriate theory. Roughly speaking, an algebraic theory consists of a specification of operations and laws that these operations must satisfy. \hypertarget{categorical_formulation}{}\subsubsection*{{Categorical formulation}}\label{categorical_formulation} Traditionally, algebraic theories were described in terms of [[logic|logical syntax]], as [[theory|first-order theories]] whose [[signatures]] have only function symbols, no relation symbols, and all of whose [[axioms]] are [[equational law]]s ([[universal quantifier|universally quantified]] [[equations]] between terms built out of these function symbols). Such descriptions may be viewed as \emph{presentations} of a theory, analogous to [[generators and relations]] as presentations of [[groups]]. In particular, different logical presentations can lead to equivalent mathematical objects. In his thesis, [[Bill Lawvere]] undertook a more invariant description of (finitary) algebraic theories. Here \emph{all} the definable operations of an algebraic theory, or rather their equivalence classes modulo the equational axioms imposed by the theory, are packaged together to form the morphisms of a category with finite products, called a [[Lawvere theory]]. None of these operations are considered ``primitive'', so a Lawvere theory doesn't play favorites among operations. This article is about generalized Lawvere theories. The article [[Lawvere theory]] treats the traditional notion of finitary, single-sorted Lawvere theories, with worked examples. The core of the present article is a working out of the precise connection between infinitary (multi-sorted) Lawvere theories and monads. \hypertarget{basic_intuitions}{}\subsubsection*{{Basic Intuitions}}\label{basic_intuitions} Intuitively, a Lawvere theory is the ``generic category of products equipped with an object $x$ of given algebraic type $T$''. For example, the Lawvere theory of groups is what you get by assuming a category with products and with a [[group object]] $x$ inside, and nothing more; $x$ can be considered ``the generic group''. Every object in the Lawvere theory is a finite power $x^n$ of the generic object $x$. The morphisms $x^n \to x$ are nothing but the $n$-ary operations it is possible to define on $x$. In other words, if we abstract away from the usual set-theoretic semantics, and consider a model for the theory of groups to be \emph{any} category with finite products together with a specified group object inside, then the Lawvere theory of groups becomes a universal model of the theory, and carries all the information of the theory but independent of a particular presentation. In this way, theories and models of a theory are placed on an equal footing. A model of a Lawvere theory $T$ in a category with products $C$ is nothing but (i.e., is equivalent to) a product-preserving functor $T \to C$; where the generic object $x$ is sent to is the given model of $T$ in $C$. If $T$ is the Lawvere theory of groups, then a product-preserving functor $T \to Set$ is tantamount to an ordinary group. The actual categorical construction of a Lawvere theory is described very easily and elegantly: it is the category opposite to the category of (finitely generated) free algebras of the theory. The free algebra on one generator becomes the generic object. If theories and models are placed on an equal footing, then what feature sets ``theories'' \emph{per se} apart? In some very abstract sense, any category with products $C$ could be considered a theory, where the $C$-models in $D$ are product-preserving functors $C \to D$. Sometimes this is a useful point of view, but it is far removed from traditional syntactic considerations. To give a more ``honest'' answer, we remember that an ordinary (finitary, single-sorted) algebraic theory a la Lawvere is generated from a single object $x$, and that every other object should be (at least up to isomorphism) a finite power $x^n$. The exponent $n$ serves to keep track of arities of operations. The generic ``category of arities'' $n$ is, in the finitary case, the category opposite to the category of finite sets (opposite because the $n$ appears contravariantly in powers $x^n$). This is also the Lawvere ``theory of equality'', or if you prefer the theory generated by an empty signature. The answer to the question ``what sets theories apart'' is that a Lawvere theory $T$ should come equipped with a product-preserving functor \begin{displaymath} x^{-}: FinSet^{op} \to T \end{displaymath} that is essentially surjective (each object of $T$ is isomorphic to $x^n$ for some arity $n$). As we see below, this definition is a cornerstone to a very elegant theory of algebraic theories. \hypertarget{extensions}{}\subsubsection*{{Extensions}}\label{extensions} \hypertarget{infinitary_operations}{}\paragraph*{{Infinitary operations}}\label{infinitary_operations} Lawvere's program can be extended to cover many theories with infinitary operations as well. In the best-behaved case, one has algebraic theories involving only operations of arity bounded by some [[cardinal number]] --- or, more precisely, belonging to some [[arity class]] --- and these can be understood category-theoretically with a suitable generalization of Lawvere theories. In this bounded case, the Lawvere theory can be described by a small category, and the category of models will be very well behaved, in particular it is a [[locally presentable category]]. In such cases there is a satisfying duality between syntax and semantics along the lines of [[Gabriel-Ulmer duality]]. Lawvere's program can to some degree be extended further: one can work with Lawvere theories which are locally small (not just small) categories. Here, the theory might not be bounded, but at least there is only a small set of operations of each arity. Examples of such large theories include \begin{itemize}% \item The theory of algebras with arbitrary sums (one model of which is $[0,\infty]$), \item The theory of sup-lattices, in which there is one operation of each arity, and \item The theory of compact Hausdorff spaces, where the operations are parametrized by ultrafilters. \end{itemize} These examples go outside the bounded (small theory) case. Locally small theories in this sense are co-extensive with the notion of monad (on $Set$): there is a free-forgetful adjunction between $Set$ and the category of models, and algebras of the theory are equivalent to algebras of the monad. In the worst case, there are algebraic theories where the number of definable operations explodes, so that there may be a proper class of operations of some fixed arity. In this case there are no free algebras, and Lawvere's reformulation no longer applies. An example is the theory of complete Boolean algebras. (Note: category theorists who define a category $U: A \to Set$ over sets to be [[algebraic category|algebraic]] if it is [[monadic functor|monadic]] would therefore not consider the variety of algebras in such cases to be ``algebraic''). Further commentary on these aspects may be found in the dozen or so comments in \href{http://golem.ph.utexas.edu/category/2009/04/report_on_88th_peripatetic_sem.html#c023188}{this thread}, dated April 13 - May 7, 2009. In summary, then, here is the connection between the logical and categorial descriptions, based on \hyperlink{Johnstone}{Johnstone}, \S{}\S{}3.7\&8. Say that a category $C$ is: \begin{itemize}% \item \emph{small algebraic} if it is given by a (small) set of operation symbols and equations; \item \emph{[[algebraic category|algebraic]]} if it is given by a monad on the category of (small) sets; \item \emph{large algebraic} if it is given by a (possibly proper) class of operation symbols and equations. \end{itemize} Then any small algebraic category is algebraic, and any algebraic category is large algebraic, but neither implication may be reversed. \hypertarget{multisorted_operations}{}\paragraph*{{Multi-sorted operations}}\label{multisorted_operations} Lawvere theories can also be generalized to handle multi-sorted operations. If $S$ is a set of sorts, then multisorted operations are of the form \begin{displaymath} \prod_{s \in S} s^{n_s} \to t \end{displaymath} so that arities are functors $n: S \to Set$, where $S$ is seen as a discrete category. Thus, an infinitary multi-sorted Lawvere theory $T$ involves an essentially surjective product-preserving functor \begin{displaymath} (Set^S)^{op} \to T \end{displaymath} and the development goes through very much as in the single-sorted case. \hypertarget{generalized_algebraic_theories}{}\paragraph*{{Generalized Algebraic Theories}}\label{generalized_algebraic_theories} See \emph{[[generalized algebraic theory]]}. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} For the moment we discuss the single-sorted case. The many-sorted case should be a straightforward extension. For any [[cardinal]] $n$, let $[n]$ be a set of that cardinality (sometimes we just use $n$). \begin{udef} A \textbf{Lawvere theory} or \textbf{algebraic theory} is a [[locally small category]] $C$ with small products that is equipped with an object $x$ such that the (unique-up-to-isomorphism) product-preserving functor \begin{displaymath} i: Set^{op} \to C: [1] \mapsto x \end{displaymath} is essentially surjective. \end{udef} \hypertarget{variations}{}\subsubsection*{{Variations}}\label{variations} Algebraic theories can be extended or specialized in various directions. Here are a few variations on the theme. \hypertarget{essentially_algebraic_theories}{}\paragraph*{{Essentially algebraic theories}}\label{essentially_algebraic_theories} \emph{[[essentially algebraic theory|Essentially algebraic theories]]} allow for partially-defined operations. Just as finitary algebraic theories can be understood as Lawvere theories, which live in the [[doctrine]] of [[cartesian monoidal category|cartesian monoidal categories]], so finitary essentially algebraic theories can be understood by a generalisation to [[finitely complete category|finitely complete categories]]. \hypertarget{multisorted_algebraic_theories}{}\paragraph*{{Multisorted algebraic theories}}\label{multisorted_algebraic_theories} \emph{[[multi-sorted theory|Multi-sorted theories]]} allow for more than one sort or type in the theory. Let $S$ be a set whose elements are called \emph{sorts}. There is a canonical map \begin{displaymath} i: S \to Ob(Set/S) \end{displaymath} which sends $s \in S$ to the object $s: 1 \to S$ in $Set/S$. Each object $U \to S$ of $Set/S$ may be thought of as a monomial term $\prod_s x_{s}^{U_s}$ where $\{x_s\}$ is a set of variables indexed by $S$, although it makes better sense to think of it that way when it is regarded as an object of $(Set/S)^{op}$. Thus, objects of $(Set/S)^{op}$ are pairs $(n, x: n \to S)$, where $n$ is any set, and morphisms $(n, x) \to (m, y)$ are functions $f: [m] \to [n]$ such that $y = x \circ f$, or $y_i = x_{f(i)}$ for all $i \in [m]$. Clearly, $(Set/S)^{op}$ has small products. In fact, any object $(n, x)$ of $(Set/S)^{op}$ is a product of objects of the form $i(s)$. \begin{prop} \label{}\hypertarget{}{} $(Set/S)^{op}$ is the free category with small products generated by the set $S$. \end{prop} \begin{proof} Let $C$ be a category with small products and let $\Phi: S \to Ob(C)$ be any function. Define a functor \begin{displaymath} \Pi: (Set/S)^{op} \to C \end{displaymath} so that $(n, x: n \to S)$ is taken to $\prod_{i \in n} \Phi(x(i))$. It is immediate that $\Pi$ is a product-preserving functor and is, up to unique isomorphism, the unique product-preserving functor that extends $\Phi$. \end{proof} \begin{def} \label{}\hypertarget{}{} A \textbf{multi-sorted algebraic theory} over the set of sorts $S$ consists of a locally small category with small products, $C$, together with a sort assignment $\Phi: S \to C$ such that the product-preserving extension \begin{displaymath} \Pi: (Set/S)^{op} \to C \end{displaymath} is essentially surjective. An \textbf{operation of arity} $x_1, \ldots, x_n \to y$ in $C$ is a morphism of the form $\Pi(n, x) \to \Phi(y)$ in $C$. If $D$ has small products, a \textbf{model} of $C$ in $D$ is a product-preserving functor $M: C \to D$. A \textbf{homomorphism of models} is simply a natural tranformation between product-preserving functors. \end{def} It is [[evil]], but nevertheless harmless and sometimes convenient, to suppose $\Pi$ is an isomorphism on objects, since we can define $C'$ to have the same objects as $Set/S$ and define hom-sets by $C'(x, y) = C(\Pi(x), \Pi(y)$. Then, the functor $(Set/S)^{op} \to C$ evidently factors as \begin{displaymath} (Set/S)^{op} \stackrel{\Pi}{\to} C' \to C \end{displaymath} where the second functor $C' \to C$ is an equivalence, so we may as well work with the functor $\Pi: (Set/S)^{op} \to C'$. \hypertarget{commutative_theories}{}\paragraph*{{Commutative theories}}\label{commutative_theories} \emph{[[commutative algebraic theory|Commutative algebraic theories]]} are (single-sorted) algebraic theories for which each operation is an algebra homomorphism. These form an important subclass. Their categories of models are [[closed monoidal category|closed]]: the [[hom sets]] have a natural model-structure (algebra-structure), and the enriched Hom-functor has a [[left adjoint]], \emph{[[tensor product]]}. The theory of complete lattices and suprema-preserving functions is an interesting (non-finitary) example. \hypertarget{RelationToMonads}{}\subsection*{{Relation to monads}}\label{RelationToMonads} We flesh out the relationships between algebraic theories and [[monads]], starting from the most general situation and then adding conditions to cut down on the size of theories. The term ``[[Lawvere theory]]'' as used here will mean a large (but locally small) [[infinitary Lawvere theory]]. (Under this relation ordinary finitary Lawvere theories correspond to \emph{[[finitary monads]]}.) \hypertarget{the_monad_of_a_locally_small_lawvere_theory}{}\subsubsection*{{The monad of a locally small Lawvere theory}}\label{the_monad_of_a_locally_small_lawvere_theory} Suppose $C$ is a (locally small, multi-sorted) Lawvere theory, so we have a product-preserving functor \begin{displaymath} \Pi: (Set/S)^{op} \to C \end{displaymath} which we may assume to be the identity on objects. We define an adjoint pair between the category of models $Mod(C, Set)$, consisting of product-preserving functors $C \to Set$ and transformations between them, and the category $Set/S$. We also denote this model category by $Prod(C, Set)$. \begin{remark} \label{}\hypertarget{}{} Observe that $(Set/S)^{op}$ is a Lawvere theory which is the theory of $S$-multi-sorted sets, \begin{displaymath} Prod((Set/S)^{op}, Set) \stackrel{- \circ i}{\simeq} Set^S \simeq Set/S, \end{displaymath} where the first equivalence obtains precisely because $(Set/S)^{op}$ is the free category with products generated by $S$. \end{remark} Let $y: C^{op} \to Mod(C, Set)$ be the Yoneda embedding, taking $c$ to the product-preserving functor $hom(c, -): C \to Set$. \begin{uthm} The functor \begin{displaymath} Set/S \stackrel{\Pi^{op}}{\to} C^{op} \stackrel{y}{\to} Mod(C, Set) \end{displaymath} is left adjoint to the functor \begin{displaymath} Prod(C, Set) \stackrel{Prod(\Pi, Set)}{\to} Prod((Set/S)^{op}, Set) \simeq Set/S \end{displaymath} (using the remark above). \end{uthm} \begin{proof} We must exhibit a natural isomorphism \begin{displaymath} Nat((y(\Pi^{op} (n \stackrel{x}{\to} S)), G) \cong Set/S(n \stackrel{x}{\to} S, G \circ \Pi \circ i) \end{displaymath} where $Nat(-, -)$ indicates the hom-functor on the functor category $Mod(C, Set)$. The left side is naturally isomorphic to \begin{displaymath} G(\Pi(n \stackrel{x}{\to} S)) \end{displaymath} by the [[Yoneda lemma]]. The right side is isomorphic to \begin{displaymath} Set/S(n \stackrel{x}{\to} S, G\Pi i) \end{displaymath} where $i: S \to (Set/S)^{op}$ is the canonical embedding. Now both $G \circ \Pi$ and $Set/S(-, G\Pi i)$ are product-preserving functors $(Set/S)^{op} \to Set$, so to check these functors are isomorphic, it suffices (by the universal property of $(Set/S)^{op}$ to check they give isomorphic results when restricted along $i$: \begin{displaymath} G \Pi i \cong Set/S(i-, G\Pi i) \end{displaymath} However, because $i: S \to (Set/S)^{op}$ is itself a Yoneda embedding $y^{op}: S \to (Set^S)^{op}$, the last isomorphism is just an instance of the Yoneda lemma, and this concludes the proof. \end{proof} The \textbf{monad of a Lawvere theory $C$} is the monad $T: Set/S \to Set/S$ associated with this adjunction. \hypertarget{large_lawvere_theory_of_a_monad}{}\subsubsection*{{Large Lawvere theory of a monad}}\label{large_lawvere_theory_of_a_monad} Now let $T: Set/S \to Set/S$ be a [[monad]] on $Set/S$, with unit $u: 1 \to T$ and multiplication $m: T T \to T$. \begin{udef} The \textbf{large Lawvere theory} $Th(T)$ \textbf{of $T$} is the [[opposite category|opposite]] of the [[Kleisli category]], $Kl(T)^{op}$. \end{udef} The left adjoint $Set/S \to Kl(T)$ is coproduct-preserving, so we have a product-preserving functor \begin{displaymath} (Set/S)^{op} \to Kl(T)^{op} \end{displaymath} which is a bijection on the classes of objects. Therefore $Kl(T)^{op}$ is indeed a (large, multi-sorted) Lawvere theory. \begin{uthm} Let $T$ be a monad on $Set/S$. The monad associated with the theory $Th(T)$ is isomorphic to $T$. \end{uthm} \begin{proof} In other words, we claim the monad of the adjunction \begin{displaymath} Set/S \stackrel{\Pi^{op}}{\to} Kl(T) \stackrel{y}{\to} Prod(Kl(T)^{op}, Set)) \dashv (Prod(Kl(T)^{op}, Set) \stackrel{Prod(\Pi, 1)}{\to} Prod((Set/S)^{op}, Set) \simeq Set/S \end{displaymath} is isomorphic to $T$. Now the functor $\Pi^{op}: Set/S \to Kl(T)$ is left adjoint to the underlying functor $U: Kl(T) \to Set/S$, and the underlying monad there is of course $T$. It is obvious that the composite \begin{displaymath} Set/S \stackrel{\Pi^{op}}{\to} Kl(T) \stackrel{y}{\to} Prod(Kl(T)^{op}, Set) \stackrel{Prod(\Pi, 1)}{\to} Prod((Set/S)^{op}, Set) \end{displaymath} takes an object $f: X \to S$ to \begin{displaymath} Kl(T)(\Pi^{op}-, \Pi(f)) \cong Set/S(-, U \Pi(f)) \cong Set/S(-, T(f)) \end{displaymath} and since the equivalence $Prod((Set/S)^{op}, Set) \to Set/S$ is adjoint to the yoneda embedding, it takes $Set/S(-, T(f))$ to $T(f)$. This proves the claim. \end{proof} In the other direction, we have \begin{uthm} Let $C$ be an $S$-sorted Lawvere theory. Then the Lawvere theory of the monad of $C$ is equivalent to $C$. \end{uthm} We assume for convenience that the product-preserving functor $\Pi: (Set/S)^{op} \to C$ is the identity on the class of objects. \begin{proof} We need to exhibit a comparison functor $Kl(T)^{op} \to C$, where $T$ is the monad of $C$. Such a comparison functor exists provided that $\Pi: (Set/S)^{op} \to C$ has a left adjoint whose associated monad is isomorphic to $T$. Now the composite \begin{displaymath} C^{op} \stackrel{y}{\to} Prod(C, Set) \stackrel{Prod(\Pi, 1)}{\to} Prod((Set/S)^{op}, Set) \end{displaymath} sends an object $c$ of $C^{op}$ to the product-preserving functor $C(c, \Pi-): (Set/S)^{op} \to Set$ which, by the remark above, is represented by an object of $Set/S$ which we denote as $U^{op} c$. In other words we have a natural isomorphism \begin{displaymath} C(c, \Pi-) \cong (Set/S)^{op}(U^{op} c, -) \end{displaymath} and by the usual Yoneda yoga, we obtained a functor $U^{op}: C \to (Set/S)^{op}$ which is left adjoint to $\Pi$. The monad $T$ is, by definition (see theorem 1) the monad associated with the adjoint pair $(\Pi^{op}: Set/S \to C) \dashv (U: C \to Set/S)$. We thus obtain the comparison functor $Kl(T)^{op} \to C$, and it is the identity on objects. On hom-sets it is given by the natural isomorphism \begin{displaymath} Kl(T)^{op}(f, g) \cong (Set/S)^{op}(f, T(g)) \cong (Set/S)^{op}(f, U\Pi^{op}(g)) \cong C(\Pi(f), \Pi(g)) \end{displaymath} and hence the comparison functor is an equivalence. \end{proof} \hypertarget{algebras_and_models}{}\subsubsection*{{Algebras and models}}\label{algebras_and_models} Each [[algebra over a monad|algebra]] $X$ of the monad $T$ gives rise to a model $M_X$ of the Lawvere theory: \begin{displaymath} Kl(T)^{op} \hookrightarrow Alg(T)^{op} \stackrel{\hom(-, X)}{\to} Set \end{displaymath} and similarly a morphism of algebras $f: X \to Y$ gives rise to a homomorphism $M_f: M_X \to M_Y$, so that we have a functor $M: Alg(T) \to Mod(Th(T), Set)$. This functor is an equivalence. It is convenient to proceed as follows. By Theorem 2, the underlying functor \begin{displaymath} Prod(Kl(T)^{op}, Set) \to Set/S \end{displaymath} has a left adjoint such that the associated monad is $T$, and this yields a comparison functor \begin{displaymath} A: Prod(Kl(T)^{op}, Set) \to Alg(T) \end{displaymath} \begin{uthm} $A$ is an equivalence. \end{uthm} \begin{proof} In outline, this proceeds as follows: \begin{itemize}% \item $A$ is essentially surjective, because if $X$ is a $T$-algebra, then $M_X: Kl(T)^{op} \to Set$ is a product-preserving functor such that $A(M_X) \cong X$. \item $A$ is full, because any algebra map $f: X \to Y$ gives rise to a model homomorphism $M_f: M_X \to M_Y$. \item $A$ is faithful. For this it suffices to prove that the underlying functor \begin{displaymath} U: Prod(Kl(T)^{op}, Set) \to Set/S \end{displaymath} is faithful. Let $f: X \to Y$ be a morphism of $Prod(Kl(T)^{op}, Set)$. Now every object of $Kl(T)^{op}$ is a product $\prod_i s_i$ of objects in the image of \begin{displaymath} S \stackrel{i}{\to} (Set/S)^{op} \to Kl(T)^{op} \end{displaymath} From the naturality of the diagram \begin{displaymath} \itexarray{ X(\prod_i s_i) & \overset{f(\prod_i s_i)}{\to} & Y(\prod_i s_i) \\ \mathllap{X(\pi)} \downarrow & & \downarrow \mathrlap{Y(\pi_i)} \\ X(s_i) & \underset{f(s_i)}{\to} & Y(s_i) } \end{displaymath} and the fact that $Y$ preserves products, we see that the component of $f$ at $\prod_i s_i$ is uniquely determined from the components $f(s): X(s) \to Y(s)$ as $s$ ranges over the image of $\Pi i: S \to Kl(T)^{op}$, in other words that the functor $U$ defined by $U(X) = X \Pi i$ is faithful. \end{itemize} Thus $A$ is an equivalence, with essential inverse $M$. \end{proof} \hypertarget{metaphor}{}\subsection*{{Metaphor}}\label{metaphor} Ring theory is a branch of mathematics with a well-developed terminology. A ring $A$ determines and is determined by an algebraic theory, whose models are left $A$-modules and whose $n$-ary operations have the form \begin{displaymath} (x_1,\ldots ,x_n) \to a_1 x_1 + \cdots + a_n x_n \end{displaymath} for some n-tuple $(a_1,\ldots ,a_n)$ of elements of $A$. We may call such an algebraic theory \textbf{annular}. The pun \emph{model/module} is due to [[Jon Beck]]. The notion that an algebraic theory is a generalized ring is often a fertile one, that automatically provides a slew of suggestive terminology and interesting problems. Many fundamental ideas of ring/module-theory are simply the restriction to annular algebraic theories of ideas that apply more widely to algebraic theories and their models. Let us denote the category of models and homomorphisms (in $Set$) of an algebraic theory $A$ by $A Mod$. Then compare the following to their counterparts in ring theory: \begin{itemize}% \item [[tensor product theory|Tensor Product of Theories]] \item [[matrix theory|Matrix Theories]] \item [[bimodel|Bimodels]] \end{itemize} \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[essentially algebraic theory]] \item \textbf{algebraic theory} / [[Lawvere theory]] / [[2-Lawvere theory]] / [[(∞,1)-algebraic theory]] \begin{itemize}% \item [[algebraic side effect]] \end{itemize} \item [[generalized algebraic theory]] \item [[globular theory]] \item [[monad]] / [[(∞,1)-monad]] \item [[operad]] / [[(∞,1)-operad]] \item [[finitely complete category]], [[cartesian functor]], [[cartesian logic]], [[cartesian theory]] \item [[regular category]], [[regular functor]], [[regular logic]], [[regular theory]], [[regular coverage]], [[regular topos]] \item [[coherent category]], [[coherent functor]], [[coherent logic]], [[coherent theory]], [[coherent coverage]], [[coherent topos]] \item [[geometric category]], \textbf{geometric functor}, [[geometric logic]], [[geometric theory]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[Peter Johnstone]], \emph{[[Stone Spaces]]} \item B. Badzioch, ``Algebraic Theories in Homotopy Theory'', Annals of Mathematics, 155, 895--913 (2002). \end{itemize} For a framework to compare different notions of algebraic theory see \begin{itemize}% \item [[Soichiro Fujii]], \emph{A unified framework for notions of algebraic theory}, (\href{https://arxiv.org/abs/1904.08541}{arXiv:1904.08541}) \end{itemize} [[!redirects algebraic theory]] [[!redirects algebraic theories]] [[!redirects finitary algebraic theory]] [[!redirects finitary algebraic theories]] \end{document}