4
$\begingroup$

The background to the following observation is standard material in categorical logic, and I thought this was was too — I don’t remember learning it, but I don’t think it is original — but I can’t now find it anywhere in the literature. Does it ring a bell to anyone? Even if it is not in print, I would be interested to know if people have heard this discussed informally, to get an idea of which communities this is folklore in.

Recall: a regular formula (over a signature $\Sigma$) is a formula constructed just from atomic formulas, finite conjunction, and existential quantification. $\newcommand{\x}{{\vec x}}\newcommand{\y}{{\vec y}}$Any regular sequent $\varphi(\x) \vdash_\x \psi(\x)$ is derivably equivalent to one in regular normal form, i.e. $\varphi'(\x) \vdash_{\vec x} \exists \y.\ \psi'(\x,\y)$, where $\varphi'$, $\psi'$ are conjunctions of atomics and $\psi'(\x,\y) \vdash_{\x,\y} \varphi'(\x)$ is derivable (this is D1.3.10 in the Elephant).

If $\varphi(\x)$ is any conjunction of atomic formulas, then there is a $\Sigma$-structure $\newcommand{\str}[2]{\langle\!\langle\, #1 \ |\ #2 \,\rangle\!\rangle } \str{\x}{\varphi}$, generated by elements for each variable in $\x$, and with the interpretation just enough to make $\varphi$ hold. This represents the interpretation of $\varphi$: for any other structure $A$, $\newcommand{\Str}{\Sigma\text{-}\mathbf{Str}}\newcommand{\interp}[2]{[\![\, #1 \ |\ #2 \,]\!] } \interp{\x}{\varphi}^A \cong \Str(\str{\x}{\varphi}, A)$.

Then (this is the fact I’m after) a structure validates a regular normal sequent $\varphi(\x) \vdash_{\vec x} \exists \y.\ \psi(\x,\y)$ just if it is injective w.r.t. the obvious map $\str{\x}{\varphi} \to \str{\x,\y}{\psi}$. Correspondingly, being a model of a regular theory $\mathbf{T}$ is a small-injectivity condition.

$\endgroup$
  • 2
    $\begingroup$ I've used the converse of this – that injectivity conditions are regular sequents – in my paper on internal homotopy theory. $\endgroup$ – Zhen Lin Feb 3 '16 at 12:45
  • $\begingroup$ @ZhenLin: ah, thankyou! Henrik Forssell also pointed out to me that the same converse appears in the Adamek/Rosicky book, in the hint to Exercise 5.e. These would be close enough to serve as a reference if there’s nothing closer, but it would be nice to have this version itself if it’s been set down somewhere. $\endgroup$ – Peter LeFanu Lumsdaine Feb 3 '16 at 13:38
  • $\begingroup$ This is a special case of Remark 5.33 in my book with Adámek which deals with small cone injectivity. $\endgroup$ – Jiří Rosický Feb 6 '16 at 9:07

Your Answer

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

Browse other questions tagged or ask your own question.