# Equivalent categories are elementarily equivalent: Formalization?

Equivalent categories should be elementarily equivalent in the sense of mathematical logic. How to make this precise? Here is an attempt:

Let $F : \mathcal{C} \to \mathcal{D}$ be an equivalence of categories. Let $\phi$ be a formula in the language of categories with $n$ free object variables and $m$ free morphism variables, with the following property: No objects are said to be equal or non-equal, and morphisms can only be said to be equal or non-equal if they have the same source and target. Then for objects $X_1,\dotsc,X_n$ and morphisms $f_1,\dotsc,f_m$ in $\mathcal{C}$, we have $$\phi^{\mathcal{C}}(X_1,\dotsc,X_n,f_1,\dotsc,f_m) \Leftrightarrow \phi^{\mathcal{D}}(F(X_1),\dotsc,F(X_n),F(f_1),\dotsc,F(f_m)).$$

The crucial assumption, in italics, shows what is really the difference between equivalences of categories and isomorphisms of categories: We cannot talk about equality of objects. And we cannot talk about equality of morphisms, unless they are parallel.

I guess the statement is more or less known and clear enough, but still not formalized enough (in terms of mathematical logic) in order to prove it properly. I guess that our language, from which $\phi$ is built, consists of two sorts, called "objects" and "morphisms" (although categories may be axiomatized with only one sort "morphisms", I doubt that this is convenient here), and that we have function symbols $s,t$ from morphisms to objects, called "source" and "target", a function symbol $\circ$ from pairs of morphisms to morphisms, called "composition", and finally a function symbol from objects to morphisms. We don't want an equality relation between objects. But we want an equality relation between parallel morphisms. I don't know how to make this precise. Somehow, in each formula, each appearance of $f=g$ should be replaced by $(f=g) \wedge s(f)=s(g) \wedge t(f)=t(g)$. But I have never heard of such replacements in mathematical logic. Is it possible to find a theory in a suitable language such that the formula $\phi$ in the statement about equivalences of categories can be any well-formed formula? Based on my own experience with category theory, there are almost no statements of the form "there is a morphism $f$ such that ...", but rather "there is a morphism $f : A \to B$". If this could be formalized, then the equality relation should be defined only between two morphisms $f : A \to B$ and $g : A \to B$. Perhaps this will be kind of a two-sorted language with "parameters"?

• Perhaps this answer referencing Categories, Allegories is of interest. Nov 15 '17 at 15:31

The question has been studied by various authors:

I'm afraid I am not familiar with the details of any of these, but I can say that FOLDS is probably the best bet. Frankly, I don't think any of these results will be especially useful – the restriction to first order logic is a severe restriction in practice. I quote Lambek's review of Freyd's paper:

How useful are the results of this paper? The ring theorist concerned with Morita equivalence of certain properties of rings must study the invariance under equivalence of certain properties of module categories. For example, he might consider such sentences as "every module is projective'' and "there exists a Noetherian generator''. It would seem that the first could in principle be handled by translating it into logical notation and checking Freyd's conditions, while the second must await an extension of Freyd's methods to non-elementary sentences. How long will ring theorists continue to wave their hands?

• Thank you for the references! I have a look at them. Mar 22 '15 at 23:53
• Since I don't have access to Freyd's article, let me mention that his result is also spelled out in "From a Geometrical Point of View: A Study of the History and Philosophy of Category Theory" by Jean-Pierre Marquis, which is available via google books. Apr 3 '15 at 19:11

The statement as you've written it down is still not true. It seems to me that you can still write down statements like "there are at least $n$ different morphisms" and these sorts of statements are not invariant under equivalence of categories (where I understand "different" to mean that either the source differs, the target difers, or the source and target are the same but the morphisms are not equal in the parallel sense).

• No, this is not a formula as stated, because $f_1 \neq f_2$ is only allowed if $f_1,f_2$ are parallel. Besides, this should be a comment, it is not an answer. Mar 22 '15 at 19:31
• @Martin: surely whatever first-order logic means, if I'm allowed to make a statement $P$ (such as $f_1 = f_2$) then I'm allowed to make the statement $\neg P$ as well. If you want to rule this out then I think you have to say more than what you've said so far. Mar 22 '15 at 19:32
• Please read my question carefully ... "morphisms can only be said to be equal if they have the same source and target.". Mar 22 '15 at 19:33
• @Martin: yes, okay, but in every flavor of logic I've seen the collection of statements I'm allowed to make is closed under negation. If you want to disallow this then, again, I think you have to say more than what you've said. Mar 22 '15 at 19:35
• @Martin: okay. Another problem: if I can't say that two objects are equal, how am I supposed to talk about composition (since naively to talk about composition I need to state the condition that some source is equal to some target)? Mar 22 '15 at 19:39