9
$\begingroup$

Recall that, in model theory, two models $M_1$ and $M_2$ of the same signature are elementary equivalent if $ M_1 \models \phi \Leftrightarrow M_2 \models \phi $ for every first order formula $\phi$ in the language.

For example, we can talk about two rings being elementary equivalent.

I'd like to know what it means for two monoidal categories $\mathcal C_1$ and $\mathcal C_2$ to be elementary equivalent.

Now, before someone jumps at me and tells me it's trivial, let me insist that I'm only going to accept an answer if it satifies the principle of equivalence (i.e., it shouldn't be evil).

So, what I'm asking is:
What, exactly, are the formulas that I'm allowed to check?

For example, the following formula is certainly not ok:
$\exists X \in \mathcal C, (X\cong 1) \wedge (X\not = 1)$

The following formula is also not ok:
$\exists X\in \mathcal C,$ the associator $a_{X,X,X}:(X\otimes X) \otimes X \to X\otimes (X \otimes X)$ is an identity morphism.

Improve this question
$\endgroup$
7
  • 5
    $\begingroup$ It has been shown independently, several time, that the class of formula that are invariant by equivalence of categories are those that are in the language that does not allows equality between object, but allow quantification on the set of objects and on sets "$Hom(X,Y)$" for fixed $X$ and $Y$. equality between arrow is allowed if they belong the same Hom set. See for example arxiv.org/abs/1004.3802 definition 3.1 and the following lemmas (other references are given there). Taking elementary equivalence in the sense of this class of formula should give you what you want, no ? $\endgroup$ – Simon Henry Jun 28 '18 at 12:27
  • $\begingroup$ Elementary equivalence is a notion for structures in the sense of Tarski. Can a monoidal category be seen as a structure in this sense? Or, how do you generalize the usual semantics (in the sense of mathematical logic) to also accomodate categories? But even before that: what about the language? how to express the axioms? - Or, are you working in some kind of type theory? $\endgroup$ – Qfwfq Jun 28 '18 at 12:29
  • 1
    $\begingroup$ So your first example is not Ok because it invole equality between object, the second example is not Ok because it involve equality between arrows that are not known to parrallel. A formula like $\exists X, \neg (X \simeq 1 ) \wedge (X \simeq X \otimes X) $ is Ok. $\endgroup$ – Simon Henry Jun 28 '18 at 12:34
  • 2
    $\begingroup$ See Makkai work on FOLDS. www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf $\endgroup$ – Eduardo Pareja Tobes Jun 28 '18 at 13:49
  • 2
    $\begingroup$ The best would be to have a look to the paper I mentioned, or to some of the other reference given here or in that paper (Makkai FOLDS is also a verion of this) for a formal definition. This idea is that one work in a "dependent type theory". with a type of object, and for each pair of object $X,Y$ a type of morphism $Hom(X,Y)$. If $f,g \in Hom(X,Y)$ then you can consider the proposition $f =g$, you are allowed to quantify over variable of type $Hom(X,Y)$, but $f \in Hom(X,Y)$ is not itself a proposition (exactly as $x \in A$ is not a proposition in multi-sorted first order logic). $\endgroup$ – Simon Henry Jun 28 '18 at 14:45
5
$\begingroup$

The question "what are the formulas that I'm allowed to check" is answered by specifying a first-order language in which to talk about monoidal categories. The language determines the formulas that are available to you.

The most natural language is a two-sorted language with sorts $O$ (for objects) and $A$ (for arrows), with function symbols $s,t: A\to O$ (source and target), $\circ\colon O\times O\to O$ (composition), $i\colon O\to A$ (identity maps), $\otimes_O\colon O\times O\to O$ (tensor product on objects), $\otimes_A\colon A\times A\to A$ (tensor product product on arrows), and a constant symbol $I\in O$. Of course, you have to decide what to do with non-composable arrows - one possibility is to replace the binary function symbol $\circ$ with a ternary relation symbol $\circ$ defining the graph of composition ($\circ(f,g,h)$ holds iff $f$ and $g$ are composable with composition $h$), while another possibility is to include "dummy elements" $*_O$ and $*_A$ in $O$ and $A$ which are the outputs of any terms which don't make sense.

As you noted, this language allows you to write down formulas which don't satisfy the principle of equivalence. In fact, any language which is expressive enough to define the relations $X\cong Y$ and $X\neq Y$ on objects will fail the principle of equivalence. There is a standard variant of first-order logic which does not have a primitive symbol $=$ for equality (this goes by the obvious name first-order logic without equality); you could try to fix this issue by removing the ability to talk about equality, at least on the object sort. But in any reasonable first-order language for categories, the relation "$f$ and $g$ are composable" will be definable on arrows, and then equality of objects $X = Y$ can be expressed by "the identity arrows $i_X$ and $i_Y$ are composable". This seems like a real obstruction to me.

It's conceivable that there's a logic $L$ which has expressivity similar to first-order logic but is only capable of expressing formulas which satisfy the principle of equivalence. I don't know such a logic, but I'm imagining one which removes equality on objects and builds the relation on arrows "$f$ and $g$ are composable" directly into the syntax. i.e. a dependent type theory where an arrow $f$ has a type $S_f\to T_f$, and the term $f\circ g$ is only well-formed when $S_f = T_g$. In any case, based on the obstruction above, I'm convinced the logic $L$ would have to have some features not present in first-order logic.

Given such a logic $L$ (and maybe the intent of your question was really "what is the logic $L$"?), you could ask about the $L$-equivalence of monoidal categories. But it would be incorrect to call this notion of equivalence elementary equivalence, since the term elementary refers specifically to first-order logic.

Improve this answer
$\endgroup$
10
  • 3
    $\begingroup$ The type of logic I describe in my comment (and which is presented in the paper of Mike Shulman I linked) is the one you are looking for. It is a first logic order so I don't see anything wrong in calling the notion "elementary equivalence". $\endgroup$ – Simon Henry Jun 28 '18 at 13:51
  • 1
    $\begingroup$ @SimonHenry Ah right, I totally forgot about FOLDS. That is indeed what I was looking for. It's a purely semantic point, but to me, dependent sorts is a feature which goes beyond first-order logic (in a way that multiple sorts does not), and I would not use the term "elementary" here. $\endgroup$ – Alex Kruckman Jun 28 '18 at 14:04
  • 1
    $\begingroup$ @SimonHenry That's an excellent point, and I've had to reflect further on my aversion to the use of the term "elementary" here. I've realized I also object to the use of "elementary" for equivalence in first-order logic without equality. For a really trivial example, any two non-empty finite sets are equivalent in first-order logic without equality, but I would never say that finite sets of different sizes are elementarily equivalent. On the flip side, if you have structures that are presented with dependent sorts, but where all sorts have equality, then these structures are essentially... $\endgroup$ – Alex Kruckman Jun 28 '18 at 14:58
  • 1
    $\begingroup$ the same as structures in an ordinary (multi-sorted) first-order language. So here I think it's ok to say "elementarily equivalent", exactly because the dependent sorts logic really has the same expressive power as the first-order logic, after the appropriate translation. But if you ban equality from some sorts, equivalence is no longer elementary. That is, for me, a category with $1$ object can never be elementarily equivalent to a category with $2$ objects, even if they're equivalent as categories. $\endgroup$ – Alex Kruckman Jun 28 '18 at 15:00
  • 1
    $\begingroup$ What about enhancing the FOLDS structure of categories to include, in addition to an equality relation on parallel arrows, a sort of isomorphisms between any two objects, together with all the relevant operations relating them to the arrows (and an equality relation on parallel isomorphisms, etc.)? That way all of the sorts would have the appropriate sort of "equality", so it would be reasonable to use the word "elementary" again. $\endgroup$ – Mike Shulman Jun 29 '18 at 4:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.