Presenting Lawvere theories? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T04:42:15Z http://mathoverflow.net/feeds/question/85193 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/85193/presenting-lawvere-theories Presenting Lawvere theories? Jacques Carette 2012-01-08T15:13:15Z 2012-08-24T14:00:26Z <p>(Re)Reading <a href="http://mathoverflow.net/questions/69086/lawvere-theories-versus-classical-universal-algebra" rel="nofollow">Lawvere theories versus classical universal algebra</a>, I was reminded of a question I have had for quite some time:</p> <blockquote> <p>What is the best way to <strong>present</strong> Lawvere theories?</p> </blockquote> <p>By <em>present</em>, I mean give a (mathematical) description of the theory, by means of <strong>syntax</strong>. The Lawvere theory will be the denotation of that syntax.</p> <p>I believe I understand the technical advantages that they provide over classical universal algebra (basically in terms of proving theorems over the models). My 'problem' is that I am trying to mechanize (parts of) mathematics. And to do that, one needs examples, which means constructing particular theories; more precisely, that means <em>writing something down, in finite terms</em> which denotes a theory.</p> <p>Lawvere theories seems to largely abstract this away, unlike classical universal algebra, which gives quite explicit tools for writing things down explicitly. With Lawvere theories, I am reduced to figuring out how to present <code>a small category with finite products such that every object is isomorphic to a finite product of copies of a distinguished object x</code>. I have read quite a bit of CT, and I have yet to find a book which gives me tools as convenient as those of universal algebra for that purpose.</p> http://mathoverflow.net/questions/85193/presenting-lawvere-theories/85198#85198 Answer by Sebastian for Presenting Lawvere theories? Sebastian 2012-01-08T16:24:11Z 2012-08-24T14:00:26Z <p>Maybe the following explanation might help a bit:</p> <p>I think you should not compare Lawvere theories with clones from universal algebra, as the two things are not on the same level of generality even within their respective field. What, in my oppinion, you should compare are </p> <p>models of Lawvere theories in Set and clones from UA,</p> <p>Lawvere theories and Abstract clones.</p> <p>Obviously, Lawvere theories describe the "abstract behaviour" of their models, the category-theoretic core, so to speak. Similarly, the abstract clone describe the abstract behaviour of the clones of universal algebra (in terms of: it gives you what function you obtain if you compose some functions; but you cannot look into the composition).</p> <p>Therefore, I do not think it makes much sense to discuss whether you should use Lawvere theories or the concrete notions from UA. The question is rather whether you would like to study models of Lawvere theories or concrete realizations of an abstract clone. </p> <p>I also find it somewhat misleading to say that you have more explicit tools in the classical framework. Depending on the category where your model is in, you might also have very explicit tools for working with them. You can look at identities (they can all be formulated in a category-theoretic way by using tuplings and projections), look at images (if the category is concrete) and you might even get something from the form of the product.</p> <p>What I am trying to say is the following: Abstract clones are equivalent to Lawvere theories and concrete clones in UA are equivalent to models in Set.</p> <p>However, and this is something that affected my personal research, looking at models in categories different from Set might even be interesting if you are only interested in clones in Set.</p> <p>To understand why that is, let us look at models without their Lawvere theory in the background, just like Universal algebraists often look at concrete clones in UA without having the corresponding abstract clone in mind. This will indicate how close the notions actually are. Let $\mathcal{C}$ be a category with an object $\mathbf{A}$ such that all finite powers of $\mathbf{A}$ also exist in $\mathcal{C}$ (apart from that, the category can be whatever you like), then we can define a clone in the following way:</p> <p>Let $O_{\mathbf{A}}^{(n)} := \mathcal{C}(\mathbf{A}^n,\mathbf{A})$ and $O_{\mathbf{A}} = \bigcup_{n \geq 0} O_{\mathbf{A}}^{(n)}$. A subset $C \subseteq O_{\mathbf{A}}$ is called a <em>clone over $\mathbf{A}$</em> if $C$ contains all projection morphisms $\pi_i \colon \mathbf{A}^n \rightarrow \mathbf{A}$ and it closed with respect to superposition in the following way: If $f_1,\ldots,f_n \in C^{(k)} (= O_{\mathbf{A}}^{(n)} \cap C)$ and $f \in C^{(n)}$, then we require $f \circ \langle f_1,\ldots,f_n \rangle \in C$.</p> <p>Cearly, this definition is just the classical definition of a clone if $\mathcal{C} = Set$ (except that the nullary operations are often excluded from the classical definition, but please let us not get into that). It is also "essentially" a model of a Lawvere theory. By that, I mean the following: A set of morphisms $C$ is a clone over the object $\mathbf{A}$ in the sense given above if any only if there exists a Lawvere theory $\mathcal{L}$ with objects $\mathbf{t_0},\mathbf{t_1},\ldots$ (where $\mathbf{t_i}$ is the $i$-th power of $\mathbf{t_1}$) and a model $M \colon \mathcal{L} \rightarrow \mathcal{C}$ such that $\mathbf{A} = M(\mathbf{t_1})$ and $C = \{ M(f) \mid f \in \mathcal{L}(\mathbf{t_n},\mathbf{t_1}) \}$.</p> <p>These thoughts at least helped me to understand the connection between models and clones as defined in UA more precisely. I, in fact, like to think of clones as I have described above, so this would be my suggestion how to present them. However, I can hardly clame that this is the best way - it depends on what you want and, of course, your personal taste. In fact, what I find most interesting is to find categories $\mathcal{C}$ and an object $\mathbf{A} \in \mathcal{C}$ such that the clone $O_{\mathbf{A}}$ is equivalent to a certain clone in $Set$, but can now be investigated differently since the categorical environment has changed. This might give universal algebraist some results that would have been much harder to get without the aforementioned change in the environment. In particular, applying duality is then possible and might be interesting (as I have tried to describe in the thread <a href="http://mathoverflow.net/questions/69086/lawvere-theories-versus-classical-universal-algebra" rel="nofollow">Lawvere theories versus classical universal algebra</a>)</p>