Hostname: page-component-5cf477f64f-tx7qf Total loading time: 0 Render date: 2025-04-06T14:25:35.840Z Has data issue: false hasContentIssue false

ENRICHED CONCEPTS OF REGULAR LOGIC

Published online by Cambridge University Press:  03 April 2025

JIŘÍ ROSICKÝ
Affiliation:
DEPARTMENT OF MATHEMATICS AND STATISTICS MASARYK UNIVERSITY FACULTY OF SCIENCES KOTLÁŘSKÁ 2, 611 37 BRNO CZECH REPUBLIC E-mail: [email protected]
GIACOMO TENDAS*
Affiliation:
DEPARTMENT OF MATHEMATICS UNIVERSITY OF MANCHESTER FACULTY OF SCIENCE AND ENGINEERING ALAN TURING BUILDING, M13 9PL MANCHESTER UK
Rights & Permissions [Opens in a new window]

Abstract

Building on our previous work on enriched universal algebra, we define a notion of enriched language consisting of function and relation symbols whose arities are objects of the base of enrichment $\mathcal {V}$. In this context, we construct atomic formulas and define the regular fragment of our enriched logic by taking conjunctions and existential quantification of those. We then characterize $\mathcal {V}$-categories of models of regular theories as enriched injectivity classes in the $\mathcal {V}$-category of structures. These notions rely on the choice of an orthogonal factorization system $(\mathcal {E},\mathcal {M})$ on $\mathcal {V}$ which will be used, in particular, to interpret relation symbols and existential quantification.

Type
Article
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s), 2025. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

1 Introduction

After considering a notion of enriched equational logic in [Reference Rosický and Tendas23], we now proceed to introduce the regular fragment of enriched logic. More precisely, we go beyond [Reference Rosický and Tendas23] by allowing our enriched languages to involve function and relation symbols whose arities are objects of the base of enrichment. Then, we introduce corresponding enriched notions of atomic formulas, as well as conjunctions and existential quantifications of such.

To achieve this, we equip the base $\mathcal {V}$ of enrichment with an enriched factorization system $(\mathcal {E},\mathcal {M})$ . We use the class $\mathcal {M}$ to interpret the relation symbols R, of a given language ${{\mathbb L}}$ , as $\mathcal {M}$ -subobjects

where X is the arity of R, and A is an object of $\mathcal {V}$ that we are endowing with an ${{\mathbb L}}$ -structure.

Building on [Reference Rosický and Tendas23], we define the $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb L}})$ of ${{\mathbb L}}$ -structures, prove that it is locally $\lambda $ -presentable as a $\mathcal {V}$ -category (when ${{\mathbb L}}$ is $\lambda $ -ary), and characterize its $\lambda $ -presentable objects.

Given a language ${{\mathbb L}}$ , we form atomic formulas out of terms, equations, and relations symbols. Then, for the fragment of logic we consider in this paper, we allow to take conjunctions and existential quantifications on these. For any ${{\mathbb L}}$ -structure A and formula $\varphi (x)$ of arity X, we define its interpretation as an $\mathcal {M}$ -subobject

this is done recursively on the construction of $\varphi $ .

The chosen factorization system is particularly important for the interpretation of existential quantification: given a formula $\psi (x,y)$ of arity $X+Y$ , we define the interpretation of $\varphi (x):=(\exists y)\psi (x,y)$ as the $(\mathcal {E},\mathcal {M})$ -factorization below.

This generalizes the interpretation of existential quantification within a topos [Reference MacLane and Moerdijk16]. In fact, in the case where $\mathcal {V}$ is a Grothendieck topos with its cartesian closed structure and equipped with the (epi, mono) factorization system, our enriched logic extends the internal logic of the topos to the case where arities are non-discrete (meaning that they are not coproducts of the terminal object in general).

Then we define sequents

$$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x)), \end{align*} $$

of formulas of the same arity X, and say that an ${{\mathbb L}}$ -structure A satisfies them if $\varphi _A\subseteq \psi _A$ as $\mathcal {M}$ -subobjects of $A^X$ . Ordinarily, regular theories are defined as set of sequents as above where $\varphi $ is a conjunction of atomic formulas and $\psi $ is a positive-primitive formula; that is, obtained by applying existential quantification to conjunctions of atomic formulas. Equivalently, one can take also $\varphi $ to be positive-primitive without changing the power of the fragment; both these notions have occurred in the literature. In the finitary setting, models of such regular theories are known to characterize finite injectivity classes in locally finitely presentable categories [Reference Adámek and Rosický1, Chapter 4], as well as those full subcategories that are closed under products, filtered colimits, and pure subobjects [Reference Rosický, Adámek and Borceux19].

In the enriched context, injectivity classes were first introduced in [Reference Lack and Rosický11] and studied for instance in [Reference Adámek and Rosický2, Reference Bourke, Lack and Vokřínek5, Reference Lack and Tendas13]. The notion relies on a class of maps $\mathcal {E}$ generalizing that of surjections; in our case this corresponds to the left class of the chosen factorization system on $\mathcal {V}$ . Then, more recently, we introduced an enriched notion of purity [Reference Rosický and Tendas22] depending on a factorization system on $\mathcal {V}$ , as in the current setting. The aim was to characterize enriched $\mathcal {E}$ -injectivity classes as those closed under a certain class of limits, filtered colimits, and $\mathcal {E}$ -pure subobjects [Reference Rosický and Tendas22, Theorem 5.5].

In this paper we shall see that, under some hypothesis on $(\mathcal {E},\mathcal {M})$ and on the given language ${{\mathbb L}}$ , the $\mathcal {E}$ -pure morphism from [Reference Rosický and Tendas22] in the $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb L}})$ can be characterized in a model theoretic way as those homomorphisms of structures $f\colon K\to L$ with are elementary with respect to every positive-primitive formula $\varphi $ (Section 6).

After this, we complete the connection with the enriched notion of injectivity, by defining our enriched regular theories to be sets of sequents of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)(\psi(x,y)\wedge \varphi(x)))\end{align*} $$

where $\varphi $ and $\psi $ are conjunctions of atomic formulas (Definition 7.1). This slightly unusual choice is dictated from the fact that, unlike in the ordinary case or the case internal to a topos, our class $\mathcal {E}$ may not be stable under pullbacks; making certain deduction rules of ordinary regular logic fail. In particular, the sequent above is not equivalent to the same sequent where $\varphi $ is omitted from the right-hand-side (Remark 4.14).

Then we can prove.

Theorem 7.6. Under Assumption 6.1, the following are equivalent for a full subcategory $\mathcal {A}$ of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ :

  1. (1) $\mathcal {A}$ is a $(\lambda ,\mathcal {E})$ -injectivity class in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ ;

  2. (2) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a regular ${\mathbb L}_{\lambda \lambda }$ -theory ${\mathbb T}$ .

The key tool for capturing $\mathcal {E}$ -injectivity in the theorem above, is proving the existence of presentation formulas for given ${{\mathbb L}}$ -structures (see [Reference Adámek and Rosický1, Remark 5.5] for the ordinary version): we say that a conjunction of atomic formulas $\varphi $ is a presentation formula for $A\in \operatorname {\mathbf {Str}}({{\mathbb L}})$ if homming out of A is isomorphic to the evaluation $\mathcal {V}$ -functor

$$ \begin{align*}\varphi_{(-)}\colon\operatorname{\mathbf{Str}}({{\mathbb L}})\longrightarrow\mathcal {V}.\end{align*} $$

The fact that these exist for any $A\in \operatorname {\mathbf {Str}}({{\mathbb L}})$ under Assumption 6.1, is discussed in Section 5.

When we are in the context of [Reference Rosický and Tendas22], so that $\mathcal {E}$ -injectivity classes can be characterized under certain closure properties, then the theorem above implies the following.

Theorem (part of Theorem 7.10).

The following are equivalent for a full subcategory $\mathcal {A}$ of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ :

  1. (1) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a regular ${\mathbb L}_{\lambda \lambda }$ -theory ${\mathbb T}$ ;

  2. (2) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a theory ${\mathbb T}$ with sequents of the form

    $$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x))\end{align*} $$
    where $\varphi $ and $\psi $ are positive-primitive ${\mathbb L}_{\lambda \lambda }$ -formulas;
  3. (3) $\mathcal {A}$ is closed under products, powers by $\mathcal {E}$ -stable objects, $\lambda $ -filtered colimits, and $\lambda $ -elementary subobjects.

The $\lambda $ -elementary morphisms are defined in Section 6, and are a natural generalization of the ordinary pure ones to the enriched context. It follows from the theorem that, in this case, one can still consider the more traditional kind of regular theories (with positive-primitive formulas on both sides of the sequents) and at the same time characterize models of such theories in terms of closure under specific limits, filtered colimits, and elementary embeddings.

Beside Grothendieck toposes, our examples of bases of enrichment include the symmetric monoidal closed categories $\operatorname {\mathbf {Met}}$ of generalized metric spaces with non-expanding maps, $\operatorname {\mathbf {Ban}}$ of Banach spaces and linear maps of norm $\leq 1$ with the factorization systems (dense, closed isometry) and (dense, isometry) respectively. In the second case, our enriched logic is related to the logic of positive bounded formulas and approximate semantics [Reference Iovino8] (see Example 4.16).

Other cases of particular interest that are covered by our theory, are those bases of enrichment for which $\mathcal {V}_0$ is a quasivariety [Reference Adámek and Rosický1] equipped with the (regular epi, mono) factorization system. Examples include the category $\operatorname {\mathbf {Ab}}$ of abelian groups, ${\mathbb R}$ - $\operatorname {\mathbf {Mod}}$ of modules over a ring R, and $\mathbf {DGAb}$ of differentially graded abelian groups.

We shall also discuss the case where $\mathcal {V}=\operatorname {\mathbf {Cat}}$ with the (surjective on objects, injective on objects and fully faithful) factorization system. In this setting, we can describe sketches, categories with limits of some type, as well as categories equipped with an abelian group bundle and small tangent categories (see [Reference Cockett and Cruttwell6, Reference Rosický20]).

2 Preliminaries

As in the setting of enriched universal algebra [Reference Rosický and Tendas23], our base of enrichment is a symmetric monoidal closed category $\mathcal {V}=(\mathcal {V}_0,\otimes ,I)$ which is locally $\lambda $ -presentable as a closed category [Reference Kelly9], for some $\lambda $ . This means that $\mathcal {V}_0$ is locally $\lambda $ -presentable and the full subcategory $\mathcal {V}_\lambda $ spanned by the $\lambda $ -presentable objects contains the unit and is closed under the monoidal structure of $\mathcal {V}_0$ . As in [Reference Rosický and Tendas23], for notational simplicity we denote by

$$ \begin{align*}A^X:=[X,A]\end{align*} $$

the internal hom in $\mathcal {V}$ . For any set X, coproducts $X\cdot I:=\sum _{x\in X}I$ of copies of I are called discrete objects of $\mathcal {V}$ . Note that, for every object V of $\mathcal {V}$ there is the induced morphism $\delta _V:V_0\to V$ where $V_0=\mathcal {V}_0(I,V)\cdot I$ .

We will make use of the enriched notions of weighted limits and colimits, for which we direct the reader to [Reference Kelly9]. In particular we will mostly consider conical limits and colimits, as well as powers and copowers (which together generate all weighted limits and colimits).

Finally, we assume our base of enrichment $\mathcal {V}$ to come equipped with an enriched (orthogonal) factorization system $(\mathcal {E},\mathcal {M})$ in the sense of [Reference Lucyshyn-Wright14]; this means that $(\mathcal {E},\mathcal {M})$ is an ordinary factorization system on $\mathcal {V}_0$ for which the class $\mathcal {E}$ is closed in the arrow $\mathcal {V}$ -category $\mathcal {V}^\to $ under copowers (or equivalently, $\mathcal {M}$ is closed under powers). We shall need the following result about such factorization systems.

Lemma 2.1. If $\mathcal {M}$ is closed in $\mathcal {V}^\to $ under $\lambda $ -filtered colimits, then $\mathcal {M}$ is locally $\lambda $ -presentable as a $\mathcal {V}$ -category and the inclusion $J\colon \mathcal {M}\hookrightarrow \mathcal {V}^\to $ has a left adjoint $L\colon \mathcal {V}^\to \to \mathcal {M}$ given pointwise by sending $f\colon X\to Y$ to the $\mathcal {M}$ -subobject $Lf\colon LX\rightarrowtail Y$ induced by the $(\mathcal {E},\mathcal {M})$ -factorization

$$ \begin{align*}X\stackrel{\mathcal {E}}{\twoheadrightarrow} LX\stackrel{\mathcal {M}}{\rightarrowtail} Y\end{align*} $$

of the map f.

Proof. The $\mathcal {V}$ -category of arrows $\mathcal {V}^\to $ is locally $\lambda $ -presentable because $\mathcal {V}$ is. Moreover $\mathcal {M}$ is closed in $\mathcal {V}^\to $ under all conical limits and powers (since $(\mathcal {E},\mathcal {M})$ is enriched); thus is closed under all weighted limits. By [Reference Adámek and Rosický1, Theorem 2.48] $J_0$ has a left adjoint, and, since J preserves powers, the ordinary left adjoint is actually an enriched one. Thus $\mathcal {M}$ is locally $\lambda $ -presentable. It is easy to see that the left adjoint acts as described in the statement.

From Section 5 this factorization system will be assumed to be proper; that is, we will assume every element of $\mathcal {E}$ to be an epimorphism and every element of $\mathcal {M}$ a monomorphism. It will also be useful to recall the following notation from [Reference Rosický and Tendas22]

Definition 2.2. An object $X\in \mathcal {V}$ is called $\mathcal {E}$ -projective if $\mathcal {V}_0(X,-)\colon \mathcal {V}_0\to \operatorname {\mathbf {Set}}$ sends maps in $\mathcal {E}$ to epimorphisms. While, X is called $\mathcal {E}$ -stable if $e^X\colon A^X\to B^X$ is in $\mathcal {E}$ whenever $e\colon A\to B$ is.

It is easy to see that if the unit is $\mathcal {E}$ -projective, every $\mathcal {E}$ -stable object is $\mathcal {E}$ -projective.

A morphism $f\colon A\to B$ in $\mathcal {V}$ is called a surjection if $\mathcal {V}_0(I,f)$ is surjective. A morphism $g\colon C\to D$ is called an injection if it has the unique right lifting property to all surjections morphisms (see [Reference Rosický21]). In what follows, $Surj$ will denote the class of surjections and $Inj$ the class of injections.

Examples 2.3. We now give a list of bases of enrichment, together with an enriched factorization system, that will be relevant to the setting of the paper.

  1. (1) $\mathcal {V}=\operatorname {\mathbf {Met}}$ where distances $\infty $ are allowed. The resulting category is locally $\aleph _1$ -presentable as a closed category and symmetric monoidal closed (where $A\otimes B$ is $A\times B$ with the metric $d((a,b),(a,b'))=d(a,a')+d(b,b')$ ). Discrete objects are discrete metric spaces (because I is the one-point metric space). As factorization systems we can take either (surjective, isometry) or (dense, closed isometry) (see [Reference Adámek and Rosický2]). Both factorization systems are enriched and proper. In the first case, I is $\mathcal {E}$ -projective while in the second case it is not $\mathcal {E}$ -projective. In both cases, $\mathcal {E}$ is closed under products in $\operatorname {\mathbf {Met}}^\to $ and discrete objects are $\mathcal {E}$ -stable. Note that the first factorization system is $(Surj,Inj)$ . We can also consider $\mathcal {V}$ to be the category $\operatorname {\mathbf {CMet}}$ of complete metric spaces. Here we only consider one factorization system given by (dense, isometry) (see [Reference Adámek and Rosický2]).

  2. (2) $\mathcal {V}=\operatorname {\mathbf {Ban}}$ the category of Banach spaces with linear maps of norm $\leq 1$ . This is symmetric monoidal closed where $\otimes $ is the projective tensor product, and internal hom is the space $[K,L]$ consisting of all bounded linear mappings (not necessarily of norm at most 1) from K to L (see [Reference Borceux4, Example 6.1.9h]). Observe that $\operatorname {\mathbf {Ban}}_0(K,L)$ is the unit ball of $[K,L]$ ; moreover, $\operatorname {\mathbf {Ban}}$ is locally $\aleph _1$ -presentable [Reference Adámek and Rosický1, Example 1.48]. The factorization system (dense, isometry) corresponds to the (epi, strong mono) factorization system, and hence it is proper. It is also enriched because isometries are closed under powers. The (strong epimorphism, monomorphism) factorization is described in [Reference Pothoven17, Section 1]; monomorphisms are one-to-one maps and strong epimorphisms are quotient maps $X\to X/Y$ where Y is a closed subspace of X. This factorization system is also enriched. Strong epimorphisms coincide with surjections. Discrete objects are coproducts of ${\mathbb C}$ (because $I={\mathbb C}$ ) and they are strong epi-projective and strong epi-stable. The unit ball functor $\operatorname {\mathbf {Ban}}_0({\mathbb C},-)\colon \operatorname {\mathbf {Ban}}\to \operatorname {\mathbf {Set}}$ has a left adjoint $l_1$ sending X to the discrete object $X\cdot {\mathbb C}$ .

  3. (3) $\mathcal {V}=\operatorname {\mathbf {Cat}}$ is cartesian closed and locally finitely presentable. The factorization system (surjective on objects, injective on objects fully faithful) coincides with $(Surj,Inj)$ . Note that this factorization system is enriched but not proper (because $1$ is not a generator). Discrete objects are discrete categories and they are $\mathcal {E}$ -stable.

  4. (4) $\mathcal {V}=\operatorname {\mathbf {Pos}}$ the cartesian closed category of posets and monotone maps, which is locally finitely presentable as a closed category. This comes equipped with the proper enriched factorization system given by $(Surj,Inj)$ . Discrete objects are $\mathcal {E}$ -stable and $\mathcal {E}$ -projective.

  5. (5) We can consider $\mathcal {V}$ to be any regular base of enrichment with the (regular epi, mono) factorization system, which is enriched and proper. The $\mathcal {E}$ -projective objects are the usual regular projectives; these are also $\mathcal {E}$ -stable if in addition $\mathcal {V}$ is a symmetric monoidal quasivariety as in [Reference Lack and Tendas12]. Examples of such a $\mathcal {V}$ include the category $\operatorname {\mathbf {Ab}}$ of abelian groups, R- $\operatorname {\mathbf {Mod}}$ of modules of a ring R, $\mathbf {GAb}$ of graded abelian groups, and $\mathbf {DGAb}$ of differentially graded abelian groups.

Within the last example falls also the case where $\mathcal {V}$ is a Grothendieck topos with its cartesian closed structure. The factorization system corresponds to the (epi, mono) one; this is the only proper factorization system in a topos (since every epimorphism is regular). The notion of regular logic we consider in this paper will extend that of (single-sorted) regular logic internal to the topos [Reference MacLane and Moerdijk16], by allowing the use of non-discrete arities.

Remark 2.4. We expect most of the results of this paper to generalize to the setting of [Reference Lucyshyn-Wright and Parker15] where the base of enrichment $\mathcal {V}$ is assumed to be locally bounded instead of locally presentable. This allows to capture other important examples of enrichment that have a more topological flavour (such as enrichment over compactly generated topological spaces). Nonetheless, we one still needs $\mathcal {V}$ to be monoidal closed, as this is fundamental for the interpretation of our enriched arities (see for instance Definition 3.4). We decided to restrict to the locally presentable case as most of the results we rely on (such as [Reference Lack and Rosický11, Reference Rosický and Tendas22, Reference Rosický and Tendas23]) assume that.

3 Enriched languages

In this section we introduce the notion of language that will be central in the development of our theory. This generalizes the concept we considered in [Reference Rosický and Tendas23] by allowing the interpretation of relation symbols. Before proceeding, we set the following assumption which is satisfied by all the examples mentioned in the preliminaries.

Assumption 3.1. We fix an enriched factorization system $(\mathcal {E},\mathcal {M})$ on $\mathcal {V}$ whose right class $\mathcal {M}$ is made of monomorphisms and is closed in $\mathcal {V}^\to $ under $\lambda $ -filtered colimits.

Remark 3.2. Note that we need to assume $\mathcal {M}$ to be contained in the class of monomorphisms of $\mathcal {V}$ as this will imply the property of Remark 3.5 below and will be needed in the proofs of Proposition 3.13 and Lemma 5.5.

As mentioned above, the following definition extends the notion of functional languages from [Reference Rosický and Tendas23] to the case where also relation symbols are allowed.

Definition 3.3. A (single-sorted) language ${\mathbb L}$ (over $\mathcal {V}$ ) is the data of:

  1. (1) a set of function symbols $f\colon (X,Y)$ whose arities X and Y are objects of $\mathcal {V}$ ;

  2. (2) a set of relation symbols $R:X$ , with arity an object X of $\mathcal {V}$ .

The language ${\mathbb L}$ is called $\lambda $ -ary if all the arities appearing in ${\mathbb L}$ lie in $\mathcal {V}_\lambda $ .

For every language ${{\mathbb L}}$ there is an associated notion of ${{\mathbb L}}$ -structure.

Definition 3.4. Given a language ${\mathbb L}$ , an ${\mathbb L}$ -structure is the data of an object $A\in \mathcal {V}$ together with:

  1. (1) a morphism $f_A\colon A^X\to A^Y$ in $\mathcal {V}$ for any function symbol $f\colon (X,Y)$ in ${\mathbb L}$ ;

  2. (2) an $\mathcal {M}$ -subobject $r_A\colon R_A\rightarrowtail A^X$ for any relation symbol $R\colon X$ in ${\mathbb L}$ .

A morphism of ${\mathbb L}$ -structures $h\colon A\to B$ is determined by a map $h\colon A\to B$ in $\mathcal {V}$ making the following square commute

for any $f\colon (X,Y)$ in ${\mathbb L}$ , and such that there exist a map $h_R\colon R_A\to R_B$ completing the diagram below

for any relation symbol $R:X$ in ${\mathbb L}$ .

Remark 3.5. Since $\mathcal {M}$ is made of monomorphisms, every map $h_R$ above is uniquely determined by the morphism h.

So far $\mathbb {L}$ -structures and morphisms between them form just an ordinary category $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ . As we did in [Reference Rosický and Tendas23], we define a $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb L}})$ whose underlying ordinary category (as the name suggests) will be the one just introduced. This will require some steps.

Note that, given a $\lambda $ -ary language ${\mathbb L}$ , we can see it as ${\mathbb L}={\mathbb F}\cup {\mathbb R}$ the union of the $\lambda $ -ary language ${\mathbb F}$ , with only the function symbols of ${\mathbb L}$ , and the $\lambda $ -ary language ${\mathbb R}$ , with only the relation symbols of ${\mathbb L}$ . Then, the $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb F}})$ of ${{\mathbb F}}$ -structures was constructed in [Reference Rosický and Tendas23, Section 3]. The next step is to construct $\operatorname {\mathbf {Str}}({{\mathbb R}})$ for the relational part of the language ${\mathbb R}$ .

Let ${\mathbb R}_{\mathcal {V}}$ the discrete $\mathcal {V}$ -category on the set ${\mathbb R}$ , and let $2_{\mathcal {V}}$ be the free $\mathcal {V}$ -category on the category $2=\{0\to 1\}$ . We can consider the $\mathcal {V}$ -category

$$ \begin{align*}2_{\mathcal {V}}\otimes{{\mathbb R}}_{\mathcal {V}}\cong \textstyle\sum_{{\mathbb R}}2_{\mathcal {V}}\end{align*} $$

and the pushout in $\mathcal {V}$ - $\operatorname {\mathbf {Cat}}$

where $i(R:X)=X$ and $j(R:X)=(1,R:X)$ . Before defining the $\mathcal {V}$ -category of ${\mathbb R}$ -structures, note that we have isomorphisms

$$ \begin{align*}[2_{\mathcal {V}}\otimes{{\mathbb R}}_{\mathcal {V}},\mathcal {V}]\cong {\prod}_{\mathbb R} [2_{\mathcal {V}},\mathcal {V}]\cong {\prod}_{\mathbb R}\mathcal {V}^\to. \end{align*} $$

Thus we can construct $\operatorname {\mathbf {Str}}({{\mathbb R}})$ as follows.

Definition 3.6. The $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb R}})$ on a $\lambda $ -ary language ${\mathbb R}$ of relation symbols is defined as the pullback

where $[H_{{\mathbb R}},\mathcal {V}]'$ is the composite of $[H_{{\mathbb R}},\mathcal {V}]$ with the isomorphisms given above, $N=\mathcal {V}(H_{{\mathbb R}}-,1)$ is fully faithful, and $J\colon \mathcal {M}\hookrightarrow \mathcal {V}^\to $ is the inclusion.

Arguing as in [Reference Rosický and Tendas23, Remark 3.4] one can show that the definition of $\operatorname {\mathbf {Str}}({{\mathbb R}})$ does not depend on the choice of $\lambda $ that makes ${{\mathbb R}}$ a $\lambda $ -ary language.

Proposition 3.7. Let ${\mathbb R}$ be a $\lambda $ -ary language of relation symbols; then:

  1. (1) the underlying category of $\operatorname {\mathbf {Str}}({{\mathbb R}})$ has ${\mathbb R}$ -structures as objects and maps of ${\mathbb R}$ -structures as morphisms;

  2. (2) $\operatorname {\mathbf {Str}}({{\mathbb R}})$ is locally $\lambda $ -presentable as a $\mathcal {V}$ -category;

  3. (3) $U_{{\mathbb R}}{\colon } \operatorname {\mathbf {Str}}({{\mathbb R}})\to \mathcal {V}\times {\prod }_{{\mathbb R}}\mathcal {M}$ is a conservative right adjoint and preserves $\lambda $ -filtered colimits.

Proof. $(1)$ By construction, an object of $\operatorname {\mathbf {Str}}({{\mathbb R}})$ is a $\mathcal {V}$ -functor $\Theta _{{\mathbb R}}\to \mathcal {V}$ whose restriction along $\theta _{{\mathbb R}}$ is isomorphic to $A^{(H_{{\mathbb R}}-)}$ for some $A\in \mathcal {V}$ , and whose restriction along $H_{{\mathbb R}}$ lands pointwise in $\mathcal {M}$ . Now, by definition of $\theta _{\mathbb R}$ , to give the data above is equivalent to give an object $A\in \mathcal {V}$ together with an ordinary functor $2\times {\mathbb R}\to \mathcal {V}_0$ which sends $(1,R:X)$ to $A^X$ , for any $(R:X)\in {\mathbb R}$ , and sends every arrow in $2\times {\mathbb R}$ to a map in $\mathcal {M}$ . In other words, it is equivalent to give an object $A\in \mathcal {V}$ together with an assignment ${\mathbb R}\to \mathcal {M}$ sending a relation $R:X$ to a map in $\mathcal {M}$ with codomain $A^X$ . This is exactly the data of an ${\mathbb R}$ -structure. The same argument applies to morphisms of the underlying category.

$(2)$ The pullback defining $\operatorname {\mathbf {Str}}({{\mathbb R}})$ is a bipullback since $([\theta _{\mathbb R},\mathcal {V}],[H_{\mathbb R},\mathcal {V}]')$ is an isofibration. Moreover, the $\mathcal {V}$ -functors $([\theta _{\mathbb R},\mathcal {V}],[H_{\mathbb R},\mathcal {V}]')$ and $N\times {\prod }_{\mathbb R} J$ are both continuous and $\lambda $ -filtered colimit preserving (by the lemma above), and the $\mathcal {V}$ -categories involved are locally $\lambda $ -presentable (for $\mathcal {M}$ this follows from Lemma 2.1, then use stability of locally $\lambda $ -presentable $\mathcal {V}$ -categories under products [Reference Bird3]). Thus $\operatorname {\mathbf {Str}}({{\mathbb R}})$ is locally $\lambda $ -presentable (again by [Reference Bird3]), and both $U_{\mathbb R}$ and $V_{\mathbb R}$ preserve all limits and $\lambda $ -filtered colimits.

$(3)$ We have already shown that $U_{\mathbb R}$ is continuous and preserves $\lambda $ -filtered colimits. Since $\mathcal {V}\times {\prod }_{\mathbb R}\mathcal {M}$ is locally presentable, then it also has a left adjoint. The fact that $U_{\mathbb R}$ is conservative follows from $(1)$ and the definition of ${\mathbb R}$ -structure.

We can now define the $\mathcal {V}$ -category of ${\mathbb L}$ -structures for a general $\lambda $ -ary language ${\mathbb L}$ .

Definition 3.8. The $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb L}})$ on a $\lambda $ -ary language ${\mathbb L}$ is defined as the pullback

where ${\mathbb L}={\mathbb F}\cup {\mathbb R}$ has been written as the union of its sub-languages of function and relation symbols respectively. We denote by $U\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to \mathcal {V}$ the diagonal of the square.

Below we denote by $V\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to {\prod }_{\mathbb R}\mathcal {M}$ the composite $U_{\mathbb R}^2\circ J_{\mathbb R}$ sending an ${\mathbb L}$ -structure A to the family $(R_A\rightarrowtail A^X)_{(R:X)}$ .

Theorem 3.9. Let ${\mathbb L}={\mathbb F}\cup {\mathbb R}$ be a $\lambda $ -ary language; then:

  1. (1) the underlying category of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ has ${\mathbb L}$ -structures as objects and maps of ${\mathbb L}$ -structures as morphisms;

  2. (2) the $\mathcal {V}$ -category $\operatorname {\mathbf {Str}}({{\mathbb L}})$ is locally $\lambda $ -presentable;

  3. (3) the forgetful $\mathcal {V}$ -functor $U\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to \mathcal {V}$ is a right adjoint and preserves $\lambda $ -filtered colimits;

  4. (4) the pair $(U,V)\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to \mathcal {V}\times {\prod }_{\mathbb R}\mathcal {M}$ is a conservative right adjoint which preserves $\lambda $ -filtered colimits.

Proof. This is obtained simply by combining [Reference Rosický and Tendas23, Proposition 3.5] and 3.7 and using the stability of locally $\lambda $ -presentable categories under bilimits [Reference Bird3] (since $U_{\mathbb F}$ and $U_{\mathbb R}$ are isofibrations, the pullback above is also a bipullback).

Let us show an example of $\mathcal {V}$ -category of structures.

Example 3.10. Let $\mathcal {V}=\mathbf {Cat}$ with the (surjective on objects, injective on objects fully faithful) factorization system. We define a relational language for the 2-category of sketches with specified shape of cones and cocones.

Given a $C\in \operatorname {\mathbf {Cat}}$ , denote by $0*C$ the category obtained by adding to C an initial object $0$ , and let $k\colon C\to 0*C$ be the inclusion. Then, given another category A, an element $x\in A^{0*C}$ is a cone over some functor $C\to A$ , while an element $y\in A^C$ is just a functor $C\to A$ . Dually, we can define $C*1$ by adding a terminal object, so that an element $x\in A^{C*1}$ is a cocone over some functor $C\to A$ .

Given small collections S and T of categories, consider the relational language ${{\mathbb R}}_{S,T}$ consisting of a relation symbol $R_C:0*C$ for any $C\in S$ and a relation symbol $R^D: D*1$ for any $D\in T$ . Then, its is easy to see that an ${{\mathbb R}}_{S,T}$ -structure is the data of a category A together with a set of cones of shape C for each $C\in S$ , and of cocones of shape $D\in T$ . This is the same as a sketch whose specified cones and cocones have shape in S and T respectively. Similarly, a morphism of ${{\mathbb R}}_{S,T}$ -structures is the same as a morphism of sketches: a functor $A\to B$ that maps specified co/cones in A into specified co/cones in B.

As a consequence $\operatorname {\mathbf {Str}}({{\mathbb R}}_{S,T})\cong \mathrm {Skt}_{S,T}$ is the 2-category of sketches with cones of shape in S and cocones of shape in T; the 2-cells in $\mathrm {Skt}_{S,T}$ are just natural transformations between the underlying functor of a morphism of sketches. By Theorem 3.9 above this is locally presentable, and in particular complete and cocomplete.

We conclude this section by characterizing the $\lambda $ -presentable objects of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ . We shall need first the following result.

Proposition 3.11. Given a language ${\mathbb L}={\mathbb F}\cup {\mathbb R}$ , the $\mathcal {V}$ -functor

$$ \begin{align*}J_{\mathbb F}\colon\operatorname{\mathbf{Str}}({{\mathbb L}})\to \operatorname{\mathbf{Str}}({{\mathbb F}}) \end{align*} $$

has both a left and a right adjoint which can be described as follows:

  • The left adjoint $F\colon \operatorname {\mathbf {Str}}({{\mathbb F}})\to \operatorname {\mathbf {Str}}({{\mathbb L}})$ takes an ${\mathbb F}$ -structure A to the ${\mathbb L}$ -structure obtained from A by interpreting the relations $R:X$ in ${\mathbb R}$ with the $\mathcal {M}$ -subobject

    $$ \begin{align*}F0\rightarrowtail A^X\end{align*} $$
    induced by the $(\mathcal {E},\mathcal {M})$ -factorization of $!\colon 0\to A^X$ .
  • The right adjoint $R\colon \operatorname {\mathbf {Str}}({{\mathbb F}})\to \operatorname {\mathbf {Str}}({{\mathbb L}})$ takes an ${\mathbb F}$ -structure A to the ${\mathbb L}$ -structure obtained from A by interpreting $R:X$ in ${\mathbb R}$ with the $\mathcal {M}$ -subobject

    $$ \begin{align*}1\colon A^X\rightarrowtail A^X\end{align*} $$
    given by the identity on $A^X$ .

Both F and R are fully faithful.

Proof. It is easy to see that F and R define respectively left and right adjoints to the underlying ordinary functor of $J_{\mathbb F}$ , and that they are fully faithful as ordinary functors. To conclude, by [Reference Kelly10, Theorem 4.85], it is enough to prove that $J_{\mathbb F}$ preserves powers and copowers by elements of $\mathcal {V}$ . The former follows by definition since $J_{\mathbb F}$ is obtained by pulling back continuous functors. For the latter, consider an ${\mathbb L}$ -structure A and some $Y\in \mathcal {V}$ ; then the copower $X\cdot A$ of A by X can be constructed by considering the copower $X\cdot J_{\mathbb FA}$ in $\operatorname {\mathbf {Str}}({{\mathbb F}})$ , and by extending it to an ${\mathbb L}$ -structure as follows: for any relation $R:Y$ we define $r_{X\cdot A}\colon R_{X\cdot A}\rightarrowtail (X\cdot A)^Y$ as the $\mathcal {M}$ -subobject obtained by taking the $(\mathcal {E},\mathcal {M})$ -factorization of the composite

$$ \begin{align*}X\cdot R_A \xrightarrow{X\cdot r_A} X\cdot (A^Y)\longrightarrow (X\cdot A)^Y\end{align*} $$

in $\mathcal {V}$ . It follows that $J_{\mathbb F}$ also preserves copowers.

In the next proposition we characterize the $\lambda $ -presentable objects of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ . We shall need the following definition.

Definition 3.12. We say that an element $A\in \mathcal {V}$ is an $\mathcal {E}$ -quotient of $Y\in \mathcal {V}$ if there exists a map $Y\twoheadrightarrow A$ in $\mathcal {E}$ .

Note that when $m\colon A\rightarrowtail B$ is in $\mathcal {M}$ and A is an $\mathcal {E}$ -quotient of the initial object $0$ , then m is induced by the $(\mathcal {E},\mathcal {M})$ -factorization of the unique map $!\colon 0\to B$ .

Proposition 3.13. An ${\mathbb L}$ -structure A is $\lambda $ -presentable in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ if and only if:

  1. (i) $J_{\mathbb {F}}(A)$ is $\lambda $ -presentable in $\operatorname {\mathbf {Str}}({{\mathbb F}})$ ;

  2. (ii) for every $R: X$ in ${{\mathbb L}}$ , its interpretation $R_A$ is an $\mathcal {E}$ -quotient of some $Y\in \mathcal {V}_\lambda $ ;

  3. (iii) all but a $\lambda $ -small number of the $R_A$ , for $R:X$ in ${\mathbb L}$ , are $\mathcal {E}$ -quotients of $0$ .

Proof. It is enough to work at the level of the underlying ordinary category $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ since enriched and ordinary finitely presentable objects coincide [Reference Kelly10, Proposition 7.5]. Let $\mathcal {G}$ be the full subcategory of $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ with objects those A satisfying the three properties above. To conclude it is enough to show (1) that every object of $\mathcal {G}$ is $\lambda $ -presentable, (2) that $\mathcal {G}$ is closed under $\lambda $ -small colimits in $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ , and (3) that $\mathcal {G}$ is strongly generating.

(1). Let $A\in \mathcal {G}$ and $h\colon A\to L:=\operatorname {colim}_iL_i$ be a morphism into a filtered colimit of objects $L_i$ in $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ , denote the colimiting cone by $(c_i\colon L_i\to L)_i$ . Since $J_{\mathbb {F}}(A)$ is $\lambda $ -presentable and $J_{\mathbb {F}}$ preserves $\lambda $ -filtered colimits, $J_{\mathbb {F}}(h)$ factors through some $J_{\mathbb {F}}(c_i)$ as a morphism $k\colon J_{\mathbb {F}}(A)\to J_{\mathbb {F}}(L_i)$ of ${\mathbb F}$ -structures. We need to extend k to a map of ${\mathbb L}$ -structures, maybe changing index i.

Going back in $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ , for every relation $R:X$ we have the solid part of diagram below

with $Y\in \mathcal {V}_\lambda $ . Now, if $Y=0$ , then $k_R$ is the unique map into $R_{L_i}$ induced by $!\colon 0\to R_{L_i}$ and the orthogonality property of the factorization system. Otherwise, since $R_L$ is the $\lambda $ -filtered colimit of the $R_{L_i}$ , the map $h_Rq$ factors through some $(c_j)_R\colon R_{L_j}\to R_L$ . Without loss of generality we can assume $i=j$ and hence we have a map $s\colon Y\to R_{L_i}$ such that $ r_{L_i}s= (k^Xr_A)q$ . Since q is in $\mathcal {E}$ and and $r_{L_i}$ in $\mathcal {M}$ , there is an induced $k_R\colon R_A\to R_{L_i}$ making the square in the diagram above commute. Since there are only a $\lambda $ -small number relations which are not $\mathcal {E}$ -quotients of $0$ , we can repeat this argument and obtain a map $k\colon A\to L_i$ in $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ such that $c_ik=h$ . By construction, any two such factorizations $k\colon A\to L_i$ and $k'\colon A\to L_j$ of h must coincide after composition with some maps $i\to l$ and $j\to l$ . This proves that A is $\lambda $ -presentable in $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ .

(2). Since $J_{\mathbb F}$ is cocontinuous, the objects of $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ satisfying the first condition are clearly closed under $\lambda $ -small colimits.

In general, given a $\lambda $ -small limit $A:=\operatorname {colim}_i(A_i)$ in $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ and a relation symbol $R:X$ in ${\mathbb L}$ , the $\mathcal {M}$ -subobject $R_A$ of $A^X$ is determined by the $(\mathcal {E},\mathcal {M})$ -factorization of the induced map $\operatorname {colim}_i(R_{A_i})\to A^X$ . It follows that $R_A$ is an $\mathcal {E}$ -quotient of $\operatorname {colim}_i(R_{A_i})$ . Thus, if each $R_{A_i}$ is an $\mathcal {E}$ -quotient of some $Y_i\in \mathcal {V}_\lambda $ , then $\operatorname {colim}_i(R_{A_i})$ is an $\mathcal {E}$ -quotient of $Y:=\sum _iY_i$ , which is still in $\mathcal {V}_\lambda $ . It follows that $R_A$ is also an $\mathcal {E}$ -quotient of Y. Thus the objects satisfying the second condition are clearly closed under $\lambda $ -small colimits.

Since $0$ is stable under $\lambda $ -small colimits, then also are its $\mathcal {E}$ -quotients (by the arguments above); therefore also the objects satisfying the third condition are closed under $\lambda $ -small colimits.

(3). Notice that, since the projections into $\operatorname {\mathbf {Str}}({{\mathbb F}})$ and into $\mathcal {M}$ (for any relation in ${\mathbb L}$ ) are jointly conservative, to show that $\mathcal {G}$ is a strong generator of $\operatorname {\mathbf {Str}}({{\mathbb L}})_0$ it is enough to show the following for any ${\mathbb L}$ -structure L. (a) That any morphism of ${\mathbb F}$ -structures $B\to J_{\mathbb F}(L)$ , with $B \lambda $ -presentable, factors through some $J_{\mathbb F}(A\to L)$ with $A\in \mathcal {G}$ . (b) That, for any relation $R:X$ , any morphism $m\to r_L$ in $\mathcal {M}$ , with $m\in \mathcal {M}_\lambda $ , factors through the R-component of some $A\to L$ with $A\in \mathcal {G}$ .

Point (a) is trivial since, by definition $J_{\mathbb F}(\mathcal {G})= \operatorname {\mathbf {Str}}({{\mathbb F}})_\lambda $ . For (b), consider a relation $R:X$ and any morphism $(u,v)\colon m\to r_L$ in $\mathcal {M}$ , with $m\colon B\rightarrowtail C$ in $\mathcal {M}_\lambda $ ; so that $u\colon B\to R_L$ , $v\colon C\to L^X$ , and $r_Lu=vm$ . Note that $m\colon B\rightarrowtail C$ is $\lambda $ -presentable in $\mathcal {M}$ if and only if $C\in \mathcal {V}_\lambda $ and B is an $\mathcal {E}$ -quotient of some $Y\in \mathcal {V}_\lambda $ .

Since we can write the ${\mathbb F}$ -structure $J_{\mathbb F}(L)$ as a $\lambda $ -filtered colimit of $\lambda $ -presentable ${\mathbb F}$ -structures, and this colimit is computed as in $\mathcal {V}$ , the map v factors through some $h^X\colon A^X\to L^X$ arising from an $h\colon A\to L$ in $\operatorname {\mathbf {Str}}({{\mathbb F}})$ . Therefore we have the solid part of the diagram below

and we define $R_A$ to be the $(\mathcal {E},\mathcal {M})$ -factorization of the composite $B\to A^X$ and the map $h_R\colon R_A\to R_L$ is induced by orthogonality of $\mathcal {E}$ and $\mathcal {M}$ . It follows that we can extend A to an ${\mathbb L}$ -structure in $\mathcal {G}$ by defining the interpretation of $R:X$ as $R_A$ (which is an $\mathcal {E}$ -quotient of $Y\in \mathcal {V}_\lambda $ ) and setting all the other relations to be $\mathcal {E}$ -quotients of $0$ . By construction h extends to a morphism of ${\mathbb L}$ -structures which satisfies our condition.

4 Formulas

Given a language ${{\mathbb L}}$ , we will introduce enriched atomic formulas over ${{\mathbb L}}$ . Starting from these, we take conjunctions and existential quantifications and define the regular fragment of our theory. Then we define their interpretation into any ${{\mathbb L}}$ -structure using the given factorization system on $\mathcal {V}$ .

The assumptions for this section are the same as those in the previous one. Given a language ${\mathbb L}={\mathbb F}\cup {\mathbb R}$ the terms we consider are the $(X,Y)$ -ary extended ${\mathbb F}$ -terms defined in [Reference Rosický and Tendas23, Section 4]; these include (but may not restrict to) the recursively generated ones of [Reference Rosický and Tendas23, Definition 4.1].

Notation 4.1. Variables have arities which are objects of $\mathcal {V}$ and we denote them as $x:X$ , for $X\in \mathcal {V}$ ; as extended terms they correspond to the identity maps between arities. Then, given an $(X,Z)$ -ary term t we write $t(x)$ to emphasize that t has input arity X. If t has input arity $X+Y$ we write $t(x,y)$ to specify that we have two input variables; this helps notationally for existential quantification.

As mentioned before, for the purposes of this paper we shall not go further the regular fragment of our logic.

Definition 4.2. Given a language ${{\mathbb L}}$ , the atomic formulas of ${{\mathbb L}}$ are defined as follows:

  1. (1) if $s,t$ are $(X,Y)$ -ary terms, then

    $$ \begin{align*}\varphi(x):=(s(x)=t(x))\end{align*} $$
    is an X-ary atomic formula;
  2. (2) if R is a X-ary relation symbol, Y is an arity, and t an $(Z,X\otimes Y)$ -ary term, then

    $$ \begin{align*}\varphi(z):= R^Y(t(z))\end{align*} $$
    is a Z-ary atomic formula.

General formulas are built recursively from atomic formulas by taking:

  1. (3) conjunctions: if $\varphi _j(x)$ are X-ary formulas, then

    $$ \begin{align*}\varphi(x):=\bigwedge\limits_{j\in J}\varphi_j\end{align*} $$
    is an X-ary formula;
  2. (4) existential quantification: if $\psi (x,y)$ is an $X+Y$ -ary formula, then

    $$ \begin{align*}\varphi(x):= (\exists y)\psi(x,y)\end{align*} $$
    is an X-ary formula.

If ${{\mathbb L}}$ is $\lambda $ -ary, the arities involved are $\lambda $ -presentable, and $|J|<\kappa $ , we get ${\mathbb L}_{\kappa \lambda }$ -formulas.

Definition 4.3. A positive-primitive formula, also called pp-formula, is one of the form

$$ \begin{align*}\varphi(x)\equiv (\exists y) \psi(x,y)\end{align*} $$

where $\psi $ is a conjunction of atomic formulas.

Next we define the interpretation of formulas in ${\mathbb L}$ -structures. The interpretation of terms is defined in [Reference Rosický and Tendas23]: an $(X,Y)$ -ary t term interprets on an ${\mathbb L}$ -structure A as a morphism $t_A\colon A^X\to A^Y$ .

Remark 4.4. If $\mathcal {V}$ is semi-cartesian (that is, the unit I is terminal) we obtain Y-ary constant symbols as function symbols of arity $(0,Y)$ .

Definition 4.5. For any ${{\mathbb L}}$ -structure A and any X-ary formula $\varphi (x)$ we define its interpretation in A as an $\mathcal {M}$ -subobject

$$ \begin{align*}\varphi_A\rightarrowtail A^X.\end{align*} $$

We argue recursively as follows:

  1. (1) If $\varphi (x)\equiv (s(x)=t(x))$ , then the interpretation $\varphi _A\rightarrowtail A^X$ is defined as the $(\mathcal {E},\mathcal {M})$ -factorization of the the equalizer of $s_A$ and $t_A$ :

  2. (2) If $\varphi (z)\equiv R^Y(t(z))$ , then the interpretation $\varphi _A\rightarrowtail A^Z$ is defined by the pullback

    where we composed $r_A^Y$ with the isomorphism $(A^X)^Y\cong A^{X\otimes Y}$ (note, the top arrow is still in $\mathcal {M}$ since it is closed under powers and pullbacks in $\mathcal {V}^\to $ ).
  3. (3) If $ \varphi (x)\equiv \bigwedge _{j\in J}\varphi _j$ , then $\varphi _A\rightarrowtail A^X$ is the intersection (wide pullback) of all the $(\varphi _j)_A\rightarrowtail A^X$ for $j\in J$ . (Since $\mathcal {M}$ is closed under intersections, this map is in $\mathcal {M}$ ).

  4. (4) If $\varphi (x)\equiv ((\exists y)\psi (x,y))$ , then $\varphi _A\rightarrowtail A^X$ is given by the $(\mathcal {E},\mathcal {M})$ -factorization below

    where the bottom composite is given by the $\mathcal {M}$ -morphism defining $\psi _A$ and the projection on the first factor.

Remark 4.6. If $(\mathcal {E},\mathcal {M})$ is proper then $\mathcal {M}$ contains the regular monomorphisms [Reference Freyd and Kelly7, Proposition 2.1.4(d)] so the interpretation of $(s(x)=t(x))$ in A coincides with the equalizer of $s_A$ and $t_A$ .

Notation 4.7. If s and t are respectively $(X,Z)$ -ary and $(Y,Z)$ -ary terms, then we denote by $(s(x)=t(y))$ the $(X+Y)$ -ary atomic formula defined by

$$ \begin{align*}(s(x)=t(y)):=(\ s(i_X(x,y))=t( i_Y(x,y))\ )\end{align*} $$

where $i_X$ and $i_Y$ are respectively the inclusions of X and Y in $X+Y$ . It is easy to see that the interpretation $\varphi _A\rightarrowtail A^{X+Y}\cong A^X\times A^Y$ is defined by the $(\mathcal {E},\mathcal {M})$ -factorization of the map

induced by the pullback of $s_A$ along $t_A$ (meaning that h is the morphism induced into the product).

Lemma 4.8. The following properties hold:

  1. (1) If $\mathcal {E}$ is closed under products in $\mathcal {V}^\to $ , then for every positive-primitive formula $\varphi $

    $$ \begin{align*}\varphi_{\prod A_i}\cong\prod\varphi_{A_i}. \end{align*} $$
  2. (2) If $X\in \mathcal {V}$ is an $\mathcal {E}$ -stable object, then for every positive-primitive formula $\varphi $

    $$ \begin{align*}\varphi_{A^X}\cong(\varphi_{A})^X. \end{align*} $$
  3. (3) If $A\cong \operatorname {colim} A_i$ is a $\lambda $ -directed colimit of ${{\mathbb L}}$ -structures, then

    $$ \begin{align*}\varphi_A\cong\operatorname{colim}\varphi_{A_i} \end{align*} $$
    for every $\lambda $ -ary positive-primitive formula $\varphi $ .

Proof. These follow directly from how we defined interpretation starting from atomic formulas, using that $(\mathcal {E},\mathcal {M})$ -factorizations are stable under the limits and colimits considered in the statement (given the additional hypotheses).

Now we turn to the notion of satisfaction.

Definition 4.9. Given an ${\mathbb L}$ -structure A, an X-ary formula $\varphi (x)$ , and an arrow $a\colon X\to A$ in $\mathcal {V}$ (a generalized element of A), we say that A satisfies $\varphi [a]$ and write

$$ \begin{align*}A\models\varphi[a]\end{align*} $$

if the transpose $\hat a\colon I\to A^X$ of a factors through $\varphi _A\rightarrowtail A^X$ .

Then we have two possible approaches to satisfaction.

Definition 4.10. Given an X-ary formula $\varphi (x)$ , we say that $A\in \operatorname {\mathbf {Str}}({{\mathbb L}})$ satisfies $\varphi (x)$ , and write

$$ \begin{align*}A\models \varphi,\end{align*} $$

if $\varphi _A\rightarrowtail A^X$ is an isomorphism. We say that A satisfies $\varphi (x)$ pointwise if $ A\models \varphi [a] $ for any $a\colon X\to A$ .

Clearly, satisfaction implies pointwise satisfaction. For the converse, we need that $\mathcal {E}$ contains the class of surjections. Indeed, if A satisfies $\varphi (x)$ pointwise, then the $\mathcal {M}$ -subobject $\varphi _A\rightarrowtail A^X$ is (a surjection and thus) in $\mathcal {E}$ , so that $\varphi _A\cong A^X$ .

We extend the satisfaction from formulas to sequents.

Definition 4.11. Given X-ary formulas $\varphi $ and $\psi $ , we say that $A\in \operatorname {\mathbf {Str}}({{\mathbb L}})$ satisfies the sequent $ (\forall x)( \varphi (x) \vdash \psi (x)), $ and write

$$ \begin{align*}A\models( \varphi\vdash \psi),\end{align*} $$

if $\varphi _A\subseteq \psi _A$ as $\mathcal {M}$ -subobjects of $A^X$ . We say that A satisfies the sequent pointwise if for any a such that $A\models \varphi [a]$ , then $A\models \psi [a]$ .

Definition 4.12. Given a set ${\mathbb T}$ of sequents, we denote by $\operatorname {\mathbf {Mod}}({\mathbb T})$ the full subcategory of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ spanned by those ${{\mathbb L}}$ -structures that satisfy the sequents in  ${\mathbb T}$ .

Remark 4.13. Note that the sequent $(\forall x)( \varphi (x) \vdash \psi (x))$ is not itself a formula in our sense. Moreover, an ${{\mathbb L}}$ -structure A is such that $A\models \varphi $ if and only if it satisfies the sequent $\top \vdash \varphi $ , where $\top $ is the empty conjunction.

Again, satisfaction implies pointwise satisfaction. While, if $\mathcal {E}$ contains the surjections, the two notions are equivalent: consider the pullback below;

if A satisfies the sequent pointwise, then f is a surjection and hence in $\mathcal {E}$ , but it is also in $\mathcal {M}$ ; thus f is an isomorphism and $\varphi _A\subseteq \psi _A$ .

The following remark shows that not all deduction rules of ordinary regular logic apply in this context; the reason is that the class of maps $\mathcal {E}$ is not stable under pullbacks in general.

Remark 4.14. Not all rules of predicate logic still apply in this enriched setting. For instance, the Frobenius condition stating that the two formulas

$$ \begin{align*}(\exists y)(\varphi(x)\wedge\psi(x,y))\ \ \ \ \ \ \text{ and }\ \ \ \ \ \ \varphi(x)\wedge(\exists y)\psi(x,y)\end{align*} $$

are equivalent, might not hold in our setting. Indeed, given an X-ary formula $\varphi $ and an $X+Y$ -ary formula $\psi $ , the interpretation of $(\varphi (x)\wedge \psi (x,y))$ in an ${{\mathbb L}}$ -structure A is given by the pullback:

Now, there are two ways in which one can take existential quantification over $y:Y$ ; we could consider either

$$ \begin{align*}\varphi(x)\wedge(\exists y)\psi(x,y)\end{align*} $$

or

$$ \begin{align*}(\exists y)(\varphi(x)\wedge\psi(x,y)).\end{align*} $$

Their interpretation in an ${{\mathbb L}}$ -structure A is given as follows

where $(\exists y \psi )_A$ is the $(\mathcal {E},\mathcal {M})$ -factorization of the bottom row of the previous diagram, and $(\exists y (\varphi \wedge \psi ))_A$ is the $(\mathcal {E},\mathcal {M})$ -factorization of the top row followed by the vertical right one (which coincides with the $(\mathcal {E},\mathcal {M})$ -factorization of the top row). The dashed arrow above exists by orthogonality of the factorization system.

It follows that in general any ${{\mathbb L}}$ -structure A satisfies the sequent

$$ \begin{align*}(\forall x)\ (\exists y)(\varphi(x)\wedge\psi(x,y))\ \vdash\ \varphi(x)\wedge(\exists y)\psi(x,y),\end{align*} $$

but need not satisfy the other implication (see below for a concrete counterexample). This will result in a non-standard choice of the notion of regular theories in Section 7. However, it is easy to see that the inverse sequent

$$ \begin{align*}(\forall x)\ \varphi(x)\wedge(\exists y)\psi(x,y)\ \vdash\ (\exists y)(\varphi(x)\wedge\psi(x,y)),\end{align*} $$

and hence the full Frobenius condition, holds with the additional assumption that $\mathcal {E}$ is stable under pullbacks.

Example 4.15. Let $\mathcal {V}=\operatorname {\mathbf {Met}}$ with the (dense, closed isometry) factorization system, where dense maps are known to not be stable under pullbacks. Consider the language ${{\mathbb L}}$ with two relation symbols $R:1$ and $S:1+1$ , so that an ${{\mathbb L}}$ -structure is a metric space M together with two closed subspaces $R_M\subseteq M$ and $S_M\subseteq M\times M$ . Within the notations of the previous remark we consider the formulas $\varphi (x)=R(x)$ and $\psi (x,y)=S(x,y)$ .

Fix then the ${{\mathbb L}}$ -structure

$$ \begin{align*}M:=({\mathbb R},R_M:=\{0\}, S_M:=\{(1/n,n)\}_{n>0});\end{align*} $$

it is easy to see that

$$ \begin{align*}(\exists y (R(x)\wedge S(x,y))_M = \emptyset\end{align*} $$

while

$$ \begin{align*}(R(x)\wedge\exists y S(x,y))_M=\{0\}\cap (\{1/n\}_{n>0}\cup\{0\})=\{0\}\end{align*} $$

so that the interpretation of the two formulas is not the same.

In the next example we show how to (partially) capture Iovino’s languages over Banach spaces [Reference Iovino8] into our context.

Example 4.16. Fix $\mathcal {V}$ to be the category $\operatorname {\mathbf {Ban}}$ of Banach spaces. Every enriched language ${\mathbb L}$ over $\operatorname {\mathbf {Ban}}$ contains a $({\mathbb C}^2,{\mathbb C})$ -ary term $+$ induced by the diagonal ${\Delta :{\mathbb C}\to {\mathbb C}^2}$ (see [Reference Rosický and Tendas23, 4.1]), as well as $({\mathbb C},{\mathbb C})$ -ary terms $c\cdot -$ for $c\in {\mathbb C}$ with $|c|\leq 1$ induced by the morphisms $c\cdot -:{\mathbb C}\to {\mathbb C}$ , and the $(0,{\mathbb C})$ -ary term induced by ${\mathbb C}\to 0$ .

For any $t>0$ , denote by ${\mathbb C}_t$ the Banach space given by ${\mathbb C}$ with norm $t\cdot |-|\colon {\mathbb C}\to {\mathbb R}$ . Then, given $B\in \operatorname {\mathbf {Ban}}$ the space $B^{{\mathbb C}_t}$ is the same as B equipped with the norm $t^{-1}\cdot \parallel \!-\!\parallel _B$ . It follows that to give a morphism $B=B^{\mathbb C}\to B^{{\mathbb C}_t}$ in $\operatorname {\mathbf {Ban}}$ is the same as giving an operator $T\colon B\to B$ of norm $\parallel \! T\!\parallel \ \leq t$ .

The languages from [Reference Iovino8] consists of sets of symbols for operators and symbols for constants, each equipped with an upper norm bound. In our setting we can see the operators as $({\mathbb C},{\mathbb C}_t)$ -ary function symbols here, t is the upper bound for the norm.

Positive bounded formulas of [Reference Iovino8] include $\parallel \! x\!\parallel \ \leq r$ and $\parallel \! x\!\parallel \ \geq r$ where r is a positive rational number. In our setting, we automatically have $\parallel \! x\!\parallel \ \leq r$ (by taking x to be ${\mathbb C}$ -ary) so that $\parallel \! x\!\parallel \ \leq r$ can be expressed as $\parallel \!\frac {1}{r}x\!\parallel \ \leq 1$ for $r\geq 1$ . For $r<1$ , we get $\parallel \! x\!\parallel \ \leq r$ by taking x to be ${\mathbb C}_r$ -ary. Formulas $\parallel \! x\!\parallel \ \geq r$ , as well as constant symbols, seem to be beyond our setting.

For positive bounded formulas, the satisfaction $\models $ from [Reference Iovino8] is our satisfaction with respect to the factorization system (strong epimorphisms, monomorphisms) while the approximate satisfaction $\models _{\mathcal {A}}$ is our satisfaction with respect to (epimorphisms, strong monomorphisms). The fact that $\models $ is stronger than $\models _{\mathcal {A}}$ corresponds to our 4.20.

Notation 4.17. Let $\psi (x,y)$ be an $X+Y$ -ary formula. We say that an ${\mathbb L}$ -structure A satisfies $(\exists !y)\psi (x,y$ ) if it satisfies the formula $(\exists y)\psi (x,y)$ and the sequent

$$ \begin{align*}(\forall x)(\forall y)(\forall y')(\psi(x,y)\wedge\psi(x,y')\ \vdash\ y=y'). \end{align*} $$

When considering a sequent of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists !y)\psi(x,y)), \end{align*} $$

we say that A satisfies it if it satisfies

$$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)\psi(x,y)), \end{align*} $$

and

$$ \begin{align*}(\forall x)(\forall y)(\forall y')( \varphi(x) \wedge \psi(x,y)\wedge\psi(x,y')\ \vdash \ y=y'). \end{align*} $$

Example 4.18. Following Example 3.10, we consider $\mathcal {V}=\mathbf {Cat}$ with the (surjective on objects, injective on objects fully faithful) factorization system. Given $C\in \mathbf {Cat}_\lambda $ we define a language ${\mathbb L}$ and formulas expressing the existence of C-limits in a category A. Since surjective on objects = surjections, satisfaction and pointwise satisfaction coincide.

Similarly to 3.10, given $C\in \operatorname {\mathbf {Cat}}_\lambda $ we define $2*C$ to be the category obtained by adding to $0*C$ a morphism $1\to 0$ with codomain the initial object of $0*C$ . We have two inclusions: $j_0,j_1\colon 0*C\to 2*C$ sending C to itself and picking out $0$ and $1$ respectively. Finally, define $i*C$ as $2*C$ where the added morphism is invertible, this also has two inclusions $l_0,l_1\colon 0*C\to i*C$ .

Now, Consider the language ${\mathbb L}$ with just a relation symbol $R:0*C$ ; for each ${\mathbb L}$ -structure A, $R_A$ should be thought of as the set of limiting cones over C. First, let us define the formula $\psi (x,z):(0*C)+(0*C)$ as below

$$ \begin{align*}\psi(x,z)\equiv \exists! (w:2*C)\ ( j_0(w)=x \wedge j_1(w)=z) \end{align*} $$

stating the existence of a unique factorization of z through x. Now we define sequents

$$ \begin{align*}\alpha\equiv (\forall x:0*C)(\forall z:0*C)\ (R(x) \wedge (k(x)=k(z))) \vdash \psi(x,z),\end{align*} $$

following the notation introduced above, then

$$ \begin{align*}\beta\equiv (\forall y:C) (\exists x:0*C)\ R(x)\wedge (k(x)=y),\end{align*} $$

and

$$ \begin{align*}\gamma\equiv (\forall w:i*C)\ R(l_0(w))\vdash R(l_1(w)).\end{align*} $$

Then $\alpha $ says that every element of R is a limiting cone, $\beta $ says that every diagram from C has a limiting cone in R, and $\gamma $ says that R contains all limiting cones. Therefore, to give an element of $\operatorname {\mathbf {Mod}}(\alpha ,\beta ,\gamma )$ is the same as to give a category A where every $C\to A$ has a limit in A; then $R_A$ is univocally determined as the full subcategory of $A^{0*C}$ spanned by the limiting cones. A morphism of models needs to preserve such full subcategories; thus sends limiting cones to limiting cones. It follows that $\operatorname {\mathbf {Mod}}(\alpha ,\beta ,\gamma )$ is the 2-category of small categories with C-limits, C-limit preserving functors, and natural transformations.

Example 4.19. Let $\mathcal {V}=\mathbf {Cat}$ and consider the functional language ${\mathbb L}_0$ with one $(1,2)$ -ary function symbol $\rho $ where $2=\{0\to 1\}$ is the arrow category. Denote $T:=i_0\circ \rho $ and consider the equation $i_1\circ \rho =\operatorname {id}$ where $i_0,i_1:1\to 2$ are inclusion. Models of this theory $E_0$ are categories A equipped with a functor $T:A\to A$ and a natural transformation $\rho :T\to \operatorname {id}_A$ (see [Reference Rosický and Tendas23, Example 5.10]).

Add $(1,2)$ -ary function symbols $+,\pi _1,\pi _2$ , denote $T_2:=i_0\circ +$ and add the equations $i_1\circ +=i_1\circ \pi _1=i_1\circ \pi _1=T$ and $i_0\circ \pi _1=i_0\circ \pi _2=T_2$ . This yields natural transformations $+,\pi _1,\pi _2:T_2\to T$ . Using Example 4.18 above, we can arrange that

is a pullback. In detail, let C be the category

giving the shape for pullbacks, and $\psi (x,z)$ be the formula of arity $(0*C)+(0*C)$ from Example 4.18; note that we have a term $t:=(\pi _1,\pi _2,\rho ,\rho )$ of arity $(1,0*C)$ which picks out the cone of shape C that we want express as a limit. Given a structure A, then $T_2$ is the pullback of $\rho $ along itself if and only if and only if for each $a\in A$ the cone $t(a):0*C\to A$ is a limit cone in A, if and only if

$$ \begin{align*}A\models \psi(tx,z),\end{align*} $$

where now $\psi (tx,z)$ has arity $1+(0*C)$ .

Using the category

we express that $+$ is associative. This makes T a semigroup bundle; that is, a semigroup in the category of functors over $\operatorname {id}$ . Hence models of the resulting theory E are categories equipped with a semigroup bundle over $\operatorname {id}$ . Morphisms are functors strictly preserving the semigroup bundles.

Similarly, we can describe categories equipped with a commutative group bundle (see [Reference Rosický20]) and categories equipped with additive bundle (= commutative monoid bundle, [Reference Cockett and Cruttwell6]). In this way, we can get tangent categories (see [Reference Cockett and Cruttwell6, Reference Rosický20]) where morphisms strictly preserve tangent structures. But right morphisms F of tangent categories seem to preserve tangent structure up to an isomorphism, i.e., $FT_1\cong T_2F$ (see [Reference Cockett and Cruttwell6]).

Remark 4.20. For a functional language, ${\mathbb L}$ -structures do not depend on the chosen factorization system $(\mathcal {E},\mathcal {M})$ . However, for a general language they do. Assume that we have factorization systems $(\mathcal {E}_0,\mathcal {M}_0)$ and $(\mathcal {E}_1,\mathcal {M}_1)$ such that $\mathcal {E}_0\subseteq \mathcal {E}_1$ , hence $\mathcal {M}_1\subseteq \mathcal {M}_0$ . Then every ${\mathbb L}$ -structure with respect to $\mathcal {M}_1$ is an ${\mathbb L}$ -structure with respect to $\mathcal {M}_0$ , giving a fully faithful inclusion

$$ \begin{align*}\operatorname{\mathbf{Str}}({\mathbb L})^1\hookrightarrow\operatorname{\mathbf{Str}}({\mathbb L})^0,\end{align*} $$

where $1$ and $0$ denote the factorization systems used to define the ${{\mathbb L}}$ -structures. Note that this reflects (but in general does not preserve) the $\lambda $ -presentable objects by 3.13.

For a conjunction $\varphi (x)$ of atomic formulas and an ${\mathbb L}$ -structure A with respect to $\mathcal {M}_1$ the satisfaction $A\models \varphi $ does not depend on the factorization system. However, if $\varphi (x)$ is positive-primitive then satisfaction $A\models \varphi $ with respect to $\mathcal {E}_0$ is stronger than that with respect to $\mathcal {E}_1$ .

5 Presentation formulas

From this section our factorization system is assumed to be proper.

Assumption 5.1. We fix a proper enriched factorization system $(\mathcal {E},\mathcal {M})$ on $\mathcal {V}$ which is closed in $\mathcal {V}^\to $ under $\lambda $ -filtered colimits.

In particular $\mathcal {M}$ contains the regular monomorphisms, and hence the interpretation of equations does not involve taking $(\mathcal {E},\mathcal {M})$ -factorizations (see Remark 4.6). This will be relevant below.

With this definition we generalize the notion of presentation formula form [Reference Adámek and Rosický1].

Definition 5.2. Given a $\lambda $ -presentable ${\mathbb L}$ -structure A, we say that an X-ary formula $\pi ^A(x)$ of ${\mathbb L}_{\lambda \lambda }$ is a presentation formula of A if for every ${\mathbb L}$ -structure B we have a bijection, natural in B, between elements $a\colon X\to B$ for which $B\models \pi ^A[a]$ and morphisms $\bar a\colon A\to B$ of ${\mathbb L}$ -structures.

We shall now give a more categorical interpretation of this definition. Every formula $\varphi $ that is a conjunction of atomic formulas, induces a $\mathcal {V}$ -functor

$$ \begin{align*}\varphi_{(-)}\colon \operatorname{\mathbf{Str}}({{\mathbb L}})\longrightarrow \mathcal {V}\end{align*} $$

defined by sending A to the interpretation $\varphi _A$ of $\varphi $ . This can be constructed by taking certain limits of the forgetful $\mathcal {V}$ -functors $U\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to \mathcal {V}$ and $V\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to {\prod }_{\mathbb R}\mathcal {M}$ ; the limits are those involved in the definition of interpretation (which does not involve $(\mathcal {E},\mathcal {M})$ factorizations). It follows in particular that $\varphi _{(-)}$ is always continuous.

Proposition 5.3. A conjunction of atomic formulas $\varphi (x)$ is a presentation formula for A if and only if

$$ \begin{align*}\operatorname{\mathbf{Str}}({{\mathbb L}})(A,-)\cong \varphi_{(-)}.\end{align*} $$

Proof. By definition of satisfaction, $\varphi $ is a presentation for A if and only if

$$ \begin{align*}\operatorname{\mathbf{Str}}({{\mathbb L}})_0(A,-)\cong \mathcal {V}_0(I,(\varphi_{(-)})_0).\end{align*} $$

But $\operatorname {\mathbf {Str}}({{\mathbb L}})_0(A,-)$ is by definition $\mathcal {V}_0(I,\operatorname {\mathbf {Str}}({{\mathbb L}})(A,-)_0)$ , and both $\operatorname {\mathbf {Str}}({{\mathbb L}})(A,-)$ and $\varphi _{(-)}$ preserve powers (being continuous); thus the existence of the natural isomorphism above is equivalent to having

$$ \begin{align*}\mathcal {V}_0(X,\operatorname{\mathbf{Str}}({{\mathbb L}})(A,-)_0)\cong \mathcal {V}_0(X,(\varphi_{(-)})_0)\end{align*} $$

naturally in $X\in \mathcal {V}_0$ . And this is in turn equivalent to $\operatorname {\mathbf {Str}}({{\mathbb L}})(A,-)\cong \varphi _{(-)}$ .

Corollary 5.4. Let $\varphi $ be a $\lambda $ -ary conjunction of atomic formulas in a language ${\mathbb L}$ . Then $\varphi $ is a presentation formula of some $\lambda $ -presentable object of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ .

Proof. The $\mathcal {V}$ -functor $ \varphi _{(-)}\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\longrightarrow \mathcal {V}$ is continuous and preserves $\lambda $ -filtered colimits since it is defined by taking $\lambda $ -small limits of the forgetful $\mathcal {V}$ -functors U and V. Thus $\varphi _{(-)}$ has a left adjoint, and is therefore a representable $\mathcal {V}$ -functor. It follows that the representing object A is $\lambda $ -presentable and, by the proposition above, $\varphi $ is a presentation formula for A.

Lemma 5.5. Let ${\mathbb L}={\mathbb F}\cup {\mathbb R}$ be a language whose functional part ${\mathbb F}$ has $\mathcal {E}$ -stable input arities. Then:

  1. (1) for any $g\colon A\to B$ in $\operatorname {\mathbf {Str}}({\mathbb L})$ , the $(\mathcal {E},\mathcal {M})$ factorization of the underlying morphism $Ug$ in $\mathcal {V}$ lifts to a factorization $(e,m)$ of g in $\operatorname {\mathbf {Str}}({\mathbb L})$ ;

  2. (2) $U\colon \operatorname {\mathbf {Str}}({{\mathbb L}})\to \mathcal {V}$ sends regular epimorphisms to maps in $\mathcal {E}$ .

Proof. $(1)$ . Consider a morphism $g\colon A\to B$ in $\operatorname {\mathbf {Str}}({\mathbb L})$ , and the $(\mathcal {E},\mathcal {M})$ factorization $(e\colon A\to E, m\colon E\to B)$ of $Ug$ in $\mathcal {V}$ . By [Reference Rosický and Tendas23, Lemma B.5(1)] we know that E inherits a unique notion of ${\mathbb F}$ -structure making e and m morphisms in $\operatorname {\mathbf {Str}}( {\mathbb F})$ ; thus we are left to prove that E also inherits a compatible notion of ${\mathbb R}$ -structure.

For any X-ary relation symbol R in ${\mathbb L}$ , we can consider the solid part of the diagram below in $\mathcal {V}$ .

Then we define $R_E$ , $e_R$ , and $m_R$ as the $(\mathcal {E},\mathcal {M})$ -factorization of $g_R$ , and $r_E$ as the morphism induced by orthogonality. Following [Reference Freyd and Kelly7, Proposition 2.1.4], $r_E$ is in $\mathcal {M}$ . This endows E with an ${\mathbb L}$ -structure that by construction makes e and m morphisms in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ .

$(2)$ . Given a regular epimorphism $g\colon A\to B$ in $\operatorname {\mathbf {Str}}({\mathbb L})$ we can consider the factorization $g=me$ as above. But m is a monomorphism and g is in particular an extremal epimorphism; thus m is an isomorphism and g is therefore sent to a map in $\mathcal {E}$ .

In the proposition below we say that a set of objects $\mathcal {P}$ of $\mathcal {V}_\lambda $ is an $\mathcal {E}$ -generator for $\mathcal {V}_\lambda $ if for any $X\in \mathcal {V}_\lambda $ there exists $Y\in \mathcal {P}$ and a map $e\colon Y\to X$ in $\mathcal {E}$ .

Lemma 5.6. Assume that $\mathcal {V}_\lambda $ has an $\mathcal {E}$ -generator of $\mathcal {E}$ -projective objects, and let ${\mathbb F}$ be a functional language with $\mathcal {E}$ -stable input arities. Then every $\lambda $ -presentable ${\mathbb F}$ -structure A can be presented as a coequalizer

of morphisms between free algebras over $\lambda $ -presentable objects $Z'$ and Z of $\mathcal {V}$ .

Proof. Let $\mathcal {G}$ be the full subcategory of $\operatorname {\mathbf {Str}}({\mathbb F})$ spanned by these objects. We need to prove that it consists of all the $\lambda $ -presentable objects. Clearly $\mathcal {G}\subseteq \operatorname {\mathbf {Str}}({\mathbb F})_\lambda $ and is a strong generator of $\operatorname {\mathbf {Str}}({\mathbb F})$ , since it contains the free $\lambda $ -presentable objects. Thanks to [Reference Kelly10, Theorem 7.2], to conclude it is enough to prove that $\mathcal {G}$ is closed under $\lambda $ -small weighted colimits.

Since $\lambda $ -small coproducts and copowers of free $\lambda $ -presentable objects are still free, it is easy to see that $\mathcal {G}$ is closed under these colimits. Thus we only need to consider coequalizers. Consider a pair $f,g\colon A\to B$ in $\mathcal {G}$ , then we can consider the solid part of the diagram below

where the pair $(h,k)$ presents B as a coequalizer of free $\lambda $ -presentable objects, while Z is $\lambda $ -presentable $\mathcal {E}$ -projective and r an epimorphism (this exists by hypothesis since $A\in \mathcal {G}$ and the $\mathcal {E}$ -projectives are an $\mathcal {E}$ -generator in $\mathcal {V}_\lambda $ ). Now, by the lemma above, $Uq\in \mathcal {E}$ ; therefore using the $\mathcal {E}$ -projectivity of Z we find $f',g'\colon FZ\to FW$ making the square above commute. To conclude it is enough to notice that the coequalizer of the pair

coincides with the coequalizer of $(f,g)$ .

Proposition 5.7. Assume that $\mathcal {V}_\lambda $ has an $\mathcal {E}$ -generator of $\mathcal {E}$ -projective objects. Let ${\mathbb L}= {\mathbb F}\cup {\mathbb R}$ be a $\lambda $ -ary language whose function symbols have $\mathcal {E}$ -stable input arities and relation symbols have $\mathcal {E}$ -stable arities. Then every $\lambda $ -presentable ${\mathbb L}$ -structure A has a presentation formula in ${{\mathbb L}}_{\lambda \lambda }$ .

Proof. Given a $\lambda $ -presentable ${\mathbb L}$ -structure A, we will construct its presentation formula. Since the algebraic reduct $J_{{\mathbb F}}(A)$ is a $\lambda $ -presentable, it is a coequalizer

of morphisms f and g between free algebras over $\lambda $ -presentable objects $Z'$ and Z of $\mathcal {V}$ (see 5.6). Since f and g are $(Z,Z')$ -ary terms, A satisfies the equation $f=g$ .

Now, by 3.13 there are a $\lambda $ -small number of $X_t$ -ary relations $R_t$ such that $(R_t)_A$ is an $\mathcal {E}$ -quotient $q_t:Y_t\twoheadrightarrow (R_t)_A$ of some $0\neq Y_t\in \mathcal {V}_\lambda $ . Since by hypothesis $\mathcal {V}_\lambda $ has an $\mathcal {E}$ -generator of $\mathcal {E}$ -projective objects, we can assume that each $Y_t$ is $\mathcal {E}$ -projective. It follows that for each t we have the following diagram

in $\mathcal {V}$ , where $\tau _t'$ exists since $U(h)^{X_t}$ is in $\mathcal {E}$ (by 5.5 and since $X_t$ is $\mathcal {E}$ -stable) and $Y_t$ is $\mathcal {E}$ -projective. By transposition $\tau _t'$ corresponds to a map $\tau _t"\colon F(X_t\otimes Y_t)\to FZ$ , and hence to a $(Z,X_t\otimes Y_t)$ -ary term $\tau _t$ . Now for each t, consider the Z-ary atomic formula $R_t^{Y_t}(\tau _t)$ . We shall show that the formula

$$ \begin{align*}\pi^A:=(f=g) \wedge \bigwedge\limits_{t} R_t^{Y_t}(\tau_t)\end{align*} $$

is a presentation formula for A. We need to show that for every ${\mathbb L}$ -structure B we have a bijection, natural in B, between elements $a\colon Z\to B$ for which $B\models \pi ^A[a]$ and morphisms $\bar a\colon A\to B$ of ${\mathbb L}$ -structures.

Notice first that $(f=g)_B$ is by definition the equalizer of $B^f,B^g\colon B^Z\to B^{Z'}$ and this, since $B^{(-)}\cong {\mathbb F}\mathrm {-Str}(F-,J_{\mathbb FB})$ , is isomorphic to ${\mathbb F}\mathrm {-Str}(J_{\mathbb FA},J_{\mathbb FB})$ . Thus we have a natural bijection between elements $a\colon Z\to B$ in $\mathcal {V}$ for which $B\models (f=g)[a]$ and morphisms of ${\mathbb F}$ -structures $\bar a\colon J_{\mathbb FA}\to J_{\mathbb FB}$ . To conclude it is enough to show that for such an $a\colon Z\to B$ , we have $B\models R_t^{Y_t}(\tau _t)[a]$ for all t if and only if $\bar a$ is actually a morphism of ${\mathbb L}$ -structures.

Given $a\colon Z\to B$ , denote by $a'\colon I\to B^Z$ its transpose; by naturality, we know that the transpose of the morphism

$$ \begin{align*}I\xrightarrow{\ a'\ } B^Z\xrightarrow{\ B^\tau} B^{X_t\otimes Y_t}\end{align*} $$

with respect to $Y_t$ , is the composite

$$ \begin{align*}x_t\colon Y_t\xrightarrow{\ q_t\ } (R_t)_A\xrightarrow{\ (r_t)_A\ } A^{X_t}\xrightarrow{\ \bar a^{X_t}} B^{X_t}.\end{align*} $$

Now, since $q_t$ is in $\mathcal {E}$ , the map of ${\mathbb F}$ -structure $\bar a$ extends to a map of ${\mathbb L}$ -structures if and only if $x_t\colon Y_t\to B^{X_t}$ above factors through $(r_t)_B\colon (R_t)_B\rightarrowtail B^{X_t}$ for any t (the morphism $(R_t)_A\to (R_t)_B$ is induced by the orthogonality property).

On the other hand, the interpretation of $R_t^{Y_t}(\tau _t)$ in B is given by the pullback

where we have identified $B^{X_t\otimes Y_t}$ with $(B^{X_t})^{Y_t}$ . Thus $a\colon Z\to B$ is such that $B\models R_t^{Y_t}(\tau _t)[a]$ if and only if $B^\tau \circ a'\colon I\to B^{X_t\otimes Y_t}$ factors through $(r_t)_B^{Y_t}$ . By transposing with respect to $Y_t$ , that holds if and only if $x_t\colon Y_t\to B^{X_t}$ factors through $(r_t)_B\colon (R_t)_B\rightarrowtail B^{X_t}$ . By the argument above this holds for any t if and only if $\bar a$ extends to a map of ${\mathbb L}$ -structures, concluding the proof.

Proposition 5.8. Let ${\mathbb L}=(\emptyset ,{\mathbb R})$ be a $\lambda $ -ary relational language. Then every $\lambda $ -presentable ${\mathbb L}$ -structure A has a presentation formula in ${{\mathbb L}}_{\lambda \lambda }$ .

Proof. Since the functional part of the language is trivial, by Proposition 3.13, an ${{\mathbb L}}$ -structure A is $\lambda $ -presentable if and only if A is $\lambda $ -presentable as an object of $\mathcal {V}$ and there are a $\lambda $ -small number of $X_t$ -ary relations $R_t$ such that $(R_t)_A$ is an $\mathcal {E}$ -quotient $q_t:Y_t\twoheadrightarrow (R_t)_A$ of some $0\neq Y_t\in \mathcal {V}_\lambda $ .

Thus we a can argue exactly as in Proposition 5.7 above by taking $f=g=1_A$ and $\tau ^{\prime }_t=(r_t)_A q_t$ .

Examples 5.9.

  1. (1) The category $\operatorname {\mathbf {Met}}$ with (surjective, isometry) factorization satisfies 5.1. For $\lambda>\omega $ , discrete $\lambda $ -presentable objects form a $Surj$ -generator because $\delta _X:X_0\to X$ are surjective. Since $Surj$ is closed under discrete powers, $e^X$ is a surjection provided that X is discrete and e is a surjection. Hence discrete objects are $Surj$ -stable. Therefore 5.7 applies to $\operatorname {\mathbf {Met}}$ .

  2. (2) Similarly, 5.7 applies to the category $\operatorname {\mathbf {Pos}}$ with the (surjective, embedding) factorization.

  3. (3) The category $\operatorname {\mathbf {Ban}}$ of Banach spaces and linear maps of norm $\leq 1$ with the (strong epimorphisms, monomorphism) factorization satisfies 5.1. Discrete Banach spaces are coproducts of ${\mathbb C}$ . Since $\operatorname {\mathbf {Ban}}$ is reflective in the monadic category of totally convex spaces (see [Reference Pumplün and Röhrl18]), every Banach space is a regular quotient of a discrete space ( $l_1$ is the left adjoint to the forgetful functor from totally convex spaces to sets). Thus discrete $\lambda $ -presentable objects for a (strong epimorphism)-generator. Hence 5.7 applies to $\operatorname {\mathbf {Ban}}$ .

  4. (4) If $\mathcal {V}$ is a symmetric monoidal quasivariety as in [Reference Lack and Tendas12], then $\mathcal {V}$ is locally finitely presentable, and we can consider the (regular epi, mono) factorization system. The regular projective objects form a regular generator, hence we can apply 5.7.

Remark 5.10. Assume that we have factorization systems $(\mathcal {E}_0,\mathcal {M}_0)$ and $(\mathcal {E}_1,\mathcal {M}_1)$ such that $\mathcal {E}_0\subseteq \mathcal {E}_1$ , so that we have an inclusion

$$ \begin{align*}J \colon \operatorname{\mathbf{Str}}({\mathbb L})^1\hookrightarrow\operatorname{\mathbf{Str}}({\mathbb L})^0,\end{align*} $$

as in 4.20. If every ${\mathbb L}^0$ -structure has a presentation formula with respect to $\mathcal {E}_0$ then every ${{\mathbb L}}^1$ -structure has it with respect to $\mathcal {E}_1$ as well. Indeed, it follows by 4.20, that given $A\in \operatorname {\mathbf {Str}}({{\mathbb L}})^0$ , if $\varphi $ is a presentation formula for the ${\mathbb L}^1$ -structure $JA$ , then it is also a presentation formula for A. However, since J may not preserve the $\lambda $ -presentable objects, if A is a $\lambda $ -presentable ${{\mathbb L}}^0$ -structure, the corresponding presentation formula may not be $\lambda $ -ary (but just $\mu $ -ary, where $\mu $ is such that $JA$ is $\mu $ -presentable). Note that there are always big enough $\mu $ for which J preserves $\mu $ -presentable objects [Reference Adámek and Rosický1, Theorem 2.19].

The remark above allows us to consider presentation formulas in $\operatorname {\mathbf {Met}}$ , $\operatorname {\mathbf {CMet}}$ and $\operatorname {\mathbf {Ban}}$ for the factorization system $(\mathcal {E}_1,\mathcal {M}_1)$ =(dense, isometry). Indeed, one takes $(\mathcal {E}_0,\mathcal {M}_0)=(Surj,Inj)$ , and considers the presentation formulas obtained in that setting by virtue of 5.7 and 5.8 (using that discrete objects are $\mathcal {E}_0$ -projective and $\mathcal {E}_0$ -stable); by the remark above, these are also presentation formulas with respect to the (dense, isometry) factorization system.

We conclude this section with the following lemma, which will be useful in Section 6.

Lemma 5.11. In the setting of 5.7 or 5.8, let $h\colon A\to B$ be a morphism between $\lambda $ -presentable ${\mathbb L}$ -structures, then there exist formulas $\pi ^A(x)$ , $\pi ^B(y)$ , and $\chi (x)$ in ${{\mathbb L}}_{\lambda \lambda }$ such that:

  1. (1) $\pi ^A$ and $\pi ^B$ are presentation formulas for A and B respectively;

  2. (2) $\chi (x)$ is a positive-primitive formula of the from

    $$ \begin{align*}(\exists y)(\pi^A(x)\ \wedge\ \pi^B(y)\ \wedge\ \tau(y)=\varepsilon(x));\end{align*} $$
  3. (3) every ${\mathbb L}$ -structure K satisfies the sequent

    $$ \begin{align*}(\forall x) (\chi(x) \vdash \pi^A(x));\end{align*} $$
  4. (4) for any ${\mathbb L}$ -structure K the $(\mathcal {E},\mathcal {M})$ factorization of $\operatorname {\mathbf {Str}}({\mathbb L})(h,K)$ is given by

    $$ \begin{align*}\operatorname{\mathbf{Str}}({\mathbb L})(B,K)\cong \pi^B_K\xrightarrow{\ \mathcal {E}\ } \chi_K\xrightarrow{\ \mathcal {M}\ } \pi^A_K\cong \operatorname{\mathbf{Str}}({\mathbb L})(A,K)\end{align*} $$
    where the map in $\mathcal {M}$ is induced by (3), and the map in $\mathcal {E}$ is necessarily unique.

The same holds in the setting of 5.10 for structures and formulas defined with respect to the factorization system $(\mathcal {E}_1,\mathcal {M}_1)$ , assuming that $(\mathcal {E}_0,\mathcal {M}_0)$ satisfies the hypotheses of 5.7 or 5.8 and that J preserves the $\lambda $ -presentable objects.

Proof. Assume first that ${{\mathbb L}}$ has non empty functional part (so that we are in the setting of 5.7). Let

and

be the coequalizers from the proof of 5.7. There is an $\mathcal {E}$ -projective object X and a morphism $e:X\to Z_A$ in $\mathcal {E}$ . Then $FX$ is projective with respect to $h_B$ (since $Uh_B$ is in $\mathcal {E}$ by 5.5). Thus, there is $t:FX\to FZ_B$ such that $h_Bt=hh_AF(e)$ . Let $\tau $ be the $(Z_B,X)$ -ary term corresponding to t and $\varepsilon $ be the $(Z_A,X)$ -ary term corresponding to $Fe$ . Then we take $\pi ^A$ and $\pi ^B$ as in 5.7 and define

$$ \begin{align*}\chi'(x,y):=(\pi^A(x)\ \wedge\ \pi^B(y)\ \wedge\ (\tau(y)=\varepsilon(x))\ ).\end{align*} $$

and $\chi (x):= (\exists y)\chi '(x,y)$ ; here, x is a $Z_A$ -sorted variable, y is a $Z_B$ -sorted variable and the equation $\tau (y)=\varepsilon (x)$ is in the sense of 4.7.

When the functional part of ${{\mathbb L}}$ is empty (and we are in the setting of 5.8) we define $\chi $ in the same way, noting that by 5.8 the chosen coequalizers are trivial now, so we do not need to consider an $\mathcal {E}$ -projective object covering $Z_A=A$ (hence $e=1_{A}$ and $t=h$ ).

By construction for each K we have $\operatorname {\mathbf {Str}}({\mathbb L})(A,K)\cong \pi ^A_K$ and $\operatorname {\mathbf {Str}}({\mathbb L})(B,K)\cong \pi ^B_K$ . Consider the solid part of the diagram below, where the squares (I) and (II) are pullbacks by definition, and $\chi "(x,y):= \pi ^B(y) \wedge (\tau (y)=\epsilon (x))$ .

Note that, commutativity of the outer square, plus the fact that (I) is a pullback, implies that the composite $\pi ^h_Km$ factors through $(\tau =\epsilon )_K\to K^{Z_A}$ to give a map $r'\colon \pi ^B_K\to (\tau =\epsilon )_K$ . Similarly, $r'$ factors through $\chi ^{\prime \prime }_K$ first, and then through $\chi ^{\prime }_K$ providing a morphism $r\colon \pi ^B_K\to \chi ^{\prime }_K$ for which $ nqr=m\pi ^h_K $ and $sr=\operatorname {id}$ . Since $e\in \mathcal {E}$ is (in particular) an epimorphism, then $K^e$ is a monomorphism, and hence so is s (being obtained by pulling back $K^e$ and composing with a map in $\mathcal {M}$ ). It follows that s is an isomorphism with inverse given by r. Now, by orthogonality of the factorization system there exists $g\colon \chi _K\to \pi ^A_K$ in $\mathcal {M}$ making the relevant triangles commute. This concludes the proof implying both points (3) and (4).

For the last statement of the lemma in the context of 5.10, one considers the formulas $\pi ^A(x)$ , $\pi ^B(y)$ , and $\chi (x)$ to be those obtained by applying the result above with respect to the factorization system $(\mathcal {E}_0,\mathcal {M}_0)$ . By 5.10 these still satisfy (1) and (2). Then points (3) and (4) can be proved as above.

6 Elementary morphisms and purity

In this section we study the connection between the notion of pure morphism introduced in [Reference Rosický and Tendas22] and the purely model theoretic notion of elementary morphism (Definition 6.3).

For this purpose presentation formulas will be essential, therefore we make the assumption below. While this might seem a very restrictive set of conditions, it is worth pointing out that many examples arise just by considering the empty language over $\mathcal {V}$ or just some relational language (which are always allowed under 6.1 below). We leave it to future work to understand whether these assumptions can be relaxed.

Assumption 6.1. We fix a proper enriched factorization system $(\mathcal {E}_0,\mathcal {M}_0)$ on $\mathcal {V}$ for which $\mathcal {M}_0$ is closed in $\mathcal {V}^\to $ under $\lambda $ -filtered colimits, and we assume that either of the following two conditions holds:

  • ${{\mathbb L}}={{\mathbb R}}$ is a $\lambda $ -ary relational language;

  • ${\mathbb L}=$ is a $\lambda $ -ary language whose function symbols have $\mathcal {E}_0$ -stable input arities and relation symbols have $\mathcal {E}_0$ -stable arities. Moreover $\mathcal {V}_\lambda $ has an $\mathcal {E}_0$ -generator of $\mathcal {E}_0$ -projective objects.

For the reminder of this section we fix an enriched factorization system $(\mathcal {E},\mathcal {M})$ as in 5.1, such that $\mathcal {E}_0\subseteq \mathcal {E}$ and for which the inclusion $ J \colon \operatorname {\mathbf {Str}}({\mathbb L})\hookrightarrow \operatorname {\mathbf {Str}}({\mathbb L})^0$ preserves $\lambda $ -presentable objects. Structures and formulas will be considered with respect to the factorization system $(\mathcal {E},\mathcal {M})$ .

This assumption holds for any $\mathcal {V}$ whenever the language is purely relational (one takes $(\mathcal {E}_0,\mathcal {M}_0)=(\mathcal {E},\mathcal {M})$ ). The second condition is valid whenever $\mathcal {V}$ is endowed with the $(Surj,Inj)$ factorization system by considering discrete arities (also in this case the two factorization system coincide); or when $\mathcal {V}$ is a symmetric monoidal quasivariety with the (regular epi, mono) factorization system and ${{\mathbb L}}$ has regular-projective arities (again, the two factorization system coincide). Finally, the second condition is valid in $\operatorname {\mathbf {Met}}$ and $\operatorname {\mathbf {Ban}}$ with $(\mathcal {E},\mathcal {M})$ =(dense, isometry) for languages whose arities are discrete (here we choose $(\mathcal {E}_0,\mathcal {M}_0)=(Surj,Inj)$ for $\operatorname {\mathbf {Met}}$ and $(\mathcal {E}_0,\mathcal {M}_0)=$ (strong epi, mono) for $\operatorname {\mathbf {Ban}}$ ).

Remark 6.2. Following Remark 5.10 (based on Propositions 5.7 and 5.8), every $\lambda $ -presentable ${\mathbb L}$ -structure A has a presentation formula in ${{\mathbb L}}_{\lambda \lambda }$ . This is the main reason why Assumption 6.1 needed to be made.

We proceed by introducing a notion that generalizes that of elementary embeddings from the ordinary context. See also [Reference Rosický and Tendas22, Definition A.5].

Definition 6.3. Let $f\colon K\to L$ be a morphism in $\operatorname {\mathbf {Str}}({\mathbb L})$ . We say that f is elementary with respect to a positive-primitive formula $\psi (x)$ if the induced diagram below

is a pullback. The morphism f is called $\lambda $ -elementary if it is elementary with respect to each positive-primitive formula in ${{\mathbb L}}_{\lambda \lambda }$ .

The following proposition holds without Assumption 6.1 (just Assumption 3.1 is enough); however 6.1 will be important for the main result of the section (Proposition 6.6)

Proposition 6.4. Let $f\colon K\to L$ be $\lambda $ -elementary. If L satisfies a sequent of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x)),\end{align*} $$

where $\varphi $ and $\psi $ are positive-primitive formulas in ${\mathbb L}_{\lambda \lambda }$ , then K also satisfies the same sequent.

Proof. Consider the solid part of the diagram below

where the two vertical squares are pullbacks since f is elementary with respect to $\varphi $ and $\psi $ , and the arrow $\varphi _L\to \psi _L$ is induced by the fact that L satisfies the sequent. By the universal property of pullbacks, the dashed arrow above exists, showing that also K satisfies the sequent.

Ordinarily, the $\lambda $ -elementary morphisms of ${{\mathbb L}}$ -structures can be characterized as those morphisms $g\colon K\to L$ that are $\lambda $ -pure (see [Reference Adámek and Rosický1]). The notion of purity has recently been extended to the enriched context in [Reference Rosický and Tendas22], were was studied its connection with enriched injectivity classes. We now recall this notion.

Given a $\mathcal {V}$ -category $\mathcal {K}$ and two morphisms $f\colon K\to L$ and $g\colon A\to B$ in it, we denote by $\mathcal {P}(g,L)$ the $(\mathcal {E},\mathcal {M})$ factorization below.

Let then $\mathcal {P}(g,f)$ be the pullback of $\mathcal {P}(g,L)$ along $\mathcal {K}(A,f)$ , then there is an induced map $r\colon \mathcal {K}(B,K)\to \mathcal {P}(g,f) $ as depicted below.

Definition 6.5 [Reference Rosický and Tendas22].

We say that $f\colon K\to L$ is $\mathcal {E}$ -pure with respect to g if the map r above is in $\mathcal {E}$ . We say that f is $(\lambda ,\mathcal {E})$ -pure if it is $\mathcal {E}$ -pure with respect to every $g\colon A\to B$ with A and $B\ \lambda $ -presentable.

Then, when $\mathcal {V}=\operatorname {\mathbf {Set}}$ with the (epi, mono) factorization system, one recovers the ordinary notion of purity. The cases of $\mathcal {V}=\operatorname {\mathbf {Met}},\operatorname {\mathbf {Ban}},\omega $ - $\operatorname {\mathbf {CPO}}$ , with the factorization system induced by dense maps, as well as the case where $\mathcal {V}$ is a symmetric monoidal quasivariety, with the (regular epi, mono) factorization system, were all studied in [Reference Rosický and Tendas22], where the definition above was unpacked to give a more approachable set of conditions.

The following proposition proves that the correspondence between $\lambda $ -elementary and $(\lambda ,\mathcal {E})$ -pure morphisms still holds in the enriched framework.

Proposition 6.6. A morphism $f\colon K\to L$ in $\operatorname {\mathbf {Str}}({\mathbb L})$ is $(\mathcal {E},\lambda )$ -pure if and only if it is $\lambda $ -elementary.

Proof. Let $f\colon K\to L$ be elementary with respect to positive-primitive formulas, and $g\colon A\to B$ a morphism between $\lambda $ -presentable objects. Consider $\pi ^A(x)$ , $\pi ^B(y)$ , and $\chi (x)$ as in Lemma 5.11 for g. Then the diagram defining the $\mathcal {E}$ -purity of f with respect to g becomes as below

where we used Lemma 5.11(4) for the isomorphism $\mathcal {P}(g,L)\cong \chi _L$ , and that f is elementary with respect to $\chi (x)$ for $\mathcal {P}(g,f)\cong \chi _K$ . The morphisms $\pi ^B_f$ and $\pi ^B_f$ are those induced in the sense explained at the beginning of Section 5. It follows that r is in $\mathcal {E}$ again thanks to Lemma 5.11(4); thus f is $\mathcal {E}$ -pure with respect to g.

Conversely, assume that $f\colon K\to L$ is an $(\mathcal {E},\lambda )$ -pure morphism between ${\mathbb L}$ -structures, and

$$ \begin{align*}\psi(x):= (\exists y) \varphi(x,y)\end{align*} $$

be any positive-primitive X-ary formula, where $\varphi $ is $X+Y$ -ary and a conjunction of atomic formulas. By Corollary 5.4 we find a $\lambda $ -presentable ${\mathbb L}$ -structure B such that $\varphi (x,y)$ is a presentation formula for B. Moreover the $\mathcal {V}$ -natural inclusions

$$ \begin{align*}\operatorname{\mathbf{Str}}({\mathbb L})(B,K)\cong \varphi_K\longrightarrow K^{X+Y}\cong \operatorname{\mathbf{Str}}({\mathbb L})(FX+FY,K)\end{align*} $$

are induced from a morphism $h\colon FX+FY\to B$ in $\operatorname {\mathbf {Str}}({\mathbb L})$ . Then we define $g\colon A\to B$ to be the composite

$$ \begin{align*}A:= FX \xrightarrow{\ i_1\ } FX+FY\xrightarrow{\ h\ } B.\end{align*} $$

Consider now the diagram involved in the definition of purity. By construction of B and A, the definition of $\varphi $ with respect to $\psi $ , and since by hypothesis f is $\mathcal {E}$ -pure with respect to g, that diagram becomes.

So that $\mathcal {P}(g,L)$ is the $(\mathcal {E},\mathcal {M})$ factorization of $g^*$ , which by definition is given by the composite

$$ \begin{align*}\varphi_K\to K^{X+Y}\xrightarrow{\pi_1}K^X.\end{align*} $$

Thus $\mathcal {P}(g,L)\cong \psi _K$ and hence f is elementary with respect to $\psi $ .

7 Regular theories and injectivity

In this section we compare the subcategories of models of enriched regular theories in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ with those subcategories which arise as enriched injectivity classes in the sense of [Reference Lack and Rosický11]. We keep the assumptions of 6.1 on our base $\mathcal {V}$ and the enriched factorization system $(\mathcal {E},\mathcal {M})$ on $\mathcal {V}$ .

Definition 7.1. A regular theory $\mathbb T$ is a set of sequents of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)(\psi(x,y)\wedge \varphi(x)))\end{align*} $$

where $\varphi $ and $\psi $ are conjunctions of atomic formulas in ${\mathbb L}_{\lambda \lambda }$ . We call these sequents regular.

Remark 7.2. As discussed in the introduction, these is not the most obvious generalization of the notion of regular theory from ordinary logic. This choice was made necessary by the fact that, since $\mathcal {E}$ may not be stable under pullbacks, certain deduction rules of ordinary regular logic do not hold any more. In particular the sequent above is not in general equivalent to the sequent

$$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)\psi(x,y))\end{align*} $$

(such equivalence holds whenever $\mathcal {E}$ is pullback stable, see Remark 4.14). In Theorems 7.8 and 7.10 we give conditions so that a more natural notion of regular theory can be considered; in 7.10 these condition still allow $\mathcal {E}$ not to be pullback-stable.

Regular theories capture the following sequents.

Example 7.3. Any sequent of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x)),\end{align*} $$

with $\varphi $ and $\psi $ conjunctions of atomic formulas, can be seen as a regular sequent.

Indeed, $\psi $ can be though as having arity $X+0$ , so that existential quantification on the variable $y:0$ is trivial. This way $(\exists y)(\psi \wedge \varphi )$ is the same as $\psi \wedge \varphi $ ; and it is easy to see that $A\models (\varphi \vdash \psi \wedge \varphi )$ if and only if $A\models (\varphi \vdash \psi )$ (since no existential quantification is involved).

Example 7.4. Note that the validity of the formula

$$ \begin{align*}(\forall x)(\exists y)\ \psi(x,y),\end{align*} $$

with $\psi $ a conjunction of atomic formulas, is equivalent to that of the regular sequent $(\forall x)( \top \vdash (\exists y)(\psi (x,y)\wedge \top ))$ where $\top $ is the empty conjunction. Hence this type of sentences can be considered within the framework of regular theories. These include also sentences of the form

$$ \begin{align*}(\forall x) \varphi(x),\end{align*} $$

where $\varphi $ is a conjunction of atomic formulas (taking existential quantification over $y: 0$ ).

Recall from [Reference Lack and Rosický11] that, given a morphism $h\colon A\to B$ in a $\mathcal {V}$ -category $\mathcal {K}$ , an object K is h-injective (over $\mathcal {E}$ ) if the map

$$ \begin{align*}\mathcal {K}(h,K)\colon \mathcal {K}(B,K)\to\mathcal {K}(A,K) \end{align*} $$

lies in $\mathcal {E}$ .

Definition 7.5. Given a morphism $h:A\to B$ between $\lambda $ -presentable ${\mathbb L}$ -structure A and B, we say that a regular sequent $\iota _h$ of ${\mathbb L}_{\lambda \lambda }$ is an injectivity sequent for h if a ${\mathbb L}$ -structure K is h-injective if and only if $K\models \iota _h$ .

Given a set $\mathcal {H}$ of morphisms between $\lambda $ -presentable ${\mathbb L}$ -structures, an ${\mathbb L}$ -structure K is $\mathcal {H}$ -injective if it is injective to every $h\in \mathcal {H}$ . Such classes of ${\mathbb L}$ -structures are called $\lambda $ -injectivity classes, or $(\lambda ,\mathcal {E})$ -injectivity classes if we want to stress $\mathcal {E}$ .

Theorem 7.6. Under Assumption 6.1, the following are equivalent for a full subcategory $\mathcal {A}$ of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ :

  1. (1) $\mathcal {A}$ is a $(\lambda ,\mathcal {E})$ -injectivity class in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ ;

  2. (2) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a regular ${\mathbb L}_{\lambda \lambda }$ -theory ${\mathbb T}$ .

Proof. $(1)\Rightarrow (2)$ . It is enough to show that every morphism between $\lambda $ -presentable ${\mathbb L}$ -structures has an injectivity sequent.

Let $h\colon A\to B$ be a morphism between $\lambda $ -presentable ${\mathbb L}$ -structures; then we can consider $\pi ^A(x)$ , $\pi ^B(y)$ , and $\chi (x)$ as in Lemma 5.11. We shall prove that the sequent

$$ \begin{align*}\iota_h:= (\forall x)(\pi^A(x)\vdash \chi(x) )\end{align*} $$

is an injectivity sequent for h. This sequent is clearly regular. Note that the other sequent is satisfied by any ${\mathbb L}$ -structure K by Lemma 5.11.

Let K be any ${\mathbb L}$ -structure; then K satisfies $\iota _h$ if and only if $\chi _K\cong \pi ^A_K$ as $\mathcal {M}$ -subobjects of $K^{Z_A}$ (since K always satisfies the other sequent), if and only if the map $\operatorname {\mathbf {Str}}({\mathbb L})(h,K)$ is in $\mathcal {E}$ (by point (4) of Lemma 5.11), if and only if K is injective with respect to h.

$(2)\Rightarrow (1)$ . It is enough to prove that given any sequent

$$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)(\psi(x,y)\wedge \varphi(x))),\end{align*} $$

where $\varphi $ and $\psi $ are conjunctions of atomic formulas of ${\mathbb L}_{\lambda \lambda }$ , there exists a morphism $g\colon A\to B$ between $\lambda $ -presentable ${\mathbb L}$ -structures for which: K is $\mathcal {E}$ -injective with respect to g if and only if $K\models \varphi \vdash (\exists y)(\psi \wedge \varphi )$ , for any $K\in \operatorname {\mathbf {Str}}({\mathbb L})$ .

By Corollary 5.4 there exists $\lambda $ -presentable ${\mathbb L}$ -structures A and C for which $\varphi (x)$ and $\psi (x,y)$ are presentation formulas for A and C respectively; these come together with maps $e\colon F(X)\to A$ and $e'\colon F(X+Y)\to C$ . Consider now the pushout B of e along $e'F(i_X)$ , as depicted below.

By homming into an ${\mathbb L}$ -structure K, using the definition of presentation formula, and taking the $(\mathcal {E},\mathcal {M})$ factorizations of the arrows corresponding to $e F(i_1)$ and $e' F(j_1)$ , we obtain the pullback diagram below.

Note that by orthogonality we already have an inclusion $(\exists y)(\psi \wedge \varphi )_K\subseteq \varphi _K$ .

Now, if K is $\mathcal {E}$ -injective with respect to g then $\operatorname {\mathbf {Str}}({{\mathbb L}})(g,K)$ is in $\mathcal {E}$ ; thus, by orthogonality, there exists an arrow $\varphi _K\to (\exists y)(\psi \wedge \varphi )_K$ making the square commute. This shows that $K\models \varphi \vdash (\exists y)(\psi \wedge \varphi )$ .

Conversely, if K satisfies the sequent, then $(\exists y)(\psi \wedge \varphi )_K=\varphi _K$ as $\mathcal {M}$ -subobjects of $K^X$ (since we already had the other inclusion). Thus $\operatorname {\mathbf {Str}}({{\mathbb L}})(g,K)$ is in $\mathcal {E}$ .

As a consequence we can characterize $\mathcal {E}$ -injectivity classes in $\mathcal {V}$ as classes of models of regular theories:

Corollary 7.7. Let $(\mathcal {E},\mathcal {M})$ be an enriched proper factorization system on $\mathcal {V}$ , and let ${{\mathbb L}}^\emptyset :=\emptyset $ be the empty language. Then, the following are equivalent for a full subcategory $\mathcal {A}$ of $\mathcal {V}$ :

  1. (1) $\mathcal {A}$ is a $(\lambda ,\mathcal {E})$ -injectivity class in $\mathcal {V}$ ;

  2. (2) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a regular ${\mathbb L}^\emptyset _{\lambda \lambda }$ -theory ${\mathbb T}$ .

Proof. Assumption 6.1 is always satisfied for ${{\mathbb L}}=\emptyset $ , and in that case $\operatorname {\mathbf {Str}}({{\mathbb L}})=\mathcal {V}$ . Thus the result follows from Theorem 7.6 above.

In the ordinary case, regular theories are defined as sequents of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x))\end{align*} $$

where $\varphi $ and $\psi $ are positive-primitive formulas in ${\mathbb L}_{\lambda \lambda }$ . However, we have seen above that these may not classify $\mathcal {E}$ -injectivity classes in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ . Below we shall give two conditions on $\mathcal {E}$ so that such classification will be possible.

The first condition is simply stability of $\mathcal {E}$ under pullbacks. In this case the proof of the following result is a direct applications of the constructions introduced in this paper.

Theorem 7.8. Let $\mathcal {E}$ be stable under pullbacks. Under Assumption 6.1, the following are equivalent for a full subcategory $\mathcal {A}$ of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ :

  1. (1) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a regular ${\mathbb L}_{\lambda \lambda }$ -theory ${\mathbb T}$ ;

  2. (2) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a theory ${\mathbb T}$ with sequents of the form

    $$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)\psi(x,y))\end{align*} $$
    where $\varphi $ and $\psi $ are conjunctions of atomic formulas in ${\mathbb L}_{\lambda \lambda }$ ;
  3. (3) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a theory ${\mathbb T}$ with sequents of the form

    $$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x))\end{align*} $$
    where $\varphi $ and $\psi $ are positive-primitive formulas in ${\mathbb L}_{\lambda \lambda }$ ;
  4. (4) $\mathcal {A}$ is a $(\lambda ,\mathcal {E})$ -injectivity class in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ .

Proof. The implications $(1)\Rightarrow (2)\Rightarrow (3)$ follow by definition, while $(4)\Rightarrow (1)$ follows from Theorem 7.6.

Thus, we only need to prove $(3)\Rightarrow (4)$ . For that it is enough to prove that given any sequent

$$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x)),\end{align*} $$

where $\varphi $ and $\psi $ are positive-primitive formulas of ${\mathbb L}_{\lambda \lambda }$ , there exists a morphism $g\colon A\to B$ between $\lambda $ -presentable ${\mathbb L}$ -structures for which: K is $\mathcal {E}$ -injective with respect to g if and only if $K\models \varphi \vdash \psi $ , for any $K\in \operatorname {\mathbf {Str}}({\mathbb L})$ .

Let us write $\varphi (x)\equiv (\exists y)\varphi '(x,y)$ and $\psi (x)\equiv (\exists z)\psi '(x,z)$ where $\varphi '$ and $\psi '$ are conjunctions of atomic formulas. By Corollary 5.4 there exists $\lambda $ -presentable ${\mathbb L}$ -structures A and C for which $\varphi '$ and $\psi '$ are presentation formulas for A and C respectively; these come together with maps $e\colon F(X+Y)\to A$ and $e'\colon F(X+Z)\to C$ . Consider now the pushout B below.

By homming into an ${\mathbb L}$ -structure K, using the definition of presentation formula, and taking the $(\mathcal {E},\mathcal {M})$ factorizations of the arrows corresponding to $e F(i_1)$ and $e' F(j_1)$ , we obtain the pullback diagram below.

Now, if K is $\mathcal {E}$ -injective with respect to g is follows that the composite $\operatorname {\mathbf {Str}}({{\mathbb L}})(B,K)\to \varphi _K$ above is in $\mathcal {E}$ ; thus, by orthogonality, there exists an arrow $\varphi _K\to \psi _K$ making the square commute. This shows that $K\models \varphi \vdash \psi $ .

Conversely, if K satisfies the sequent, we have a dashed arrow as in the diagram. Hence $\operatorname {\mathbf {Str}}({{\mathbb L}})(B,K)$ can be seen as the pullback of the cospan

$$ \begin{align*}\operatorname{\mathbf{Str}}({{\mathbb L}})(C,K)\twoheadrightarrow \psi_K\leftarrow \operatorname{\mathbf{Str}}({{\mathbb L}})(A,K)\end{align*} $$

since every map in $\mathcal {M}$ is a monomorphism. But $\mathcal {E}$ is pullback stable, thus $\operatorname {\mathbf {Str}}(g,K)$ is in $\mathcal {E}$ and hence K is $\mathcal {E}$ -injective with respect to g.

Pullback stability of $\mathcal {E}$ is quite restrictive, for instance dense maps in $\operatorname {\mathbf {Met}}$ or $\operatorname {\mathbf {CMet}}$ do not satisfy it (see [Reference Rosický and Tendas22, Remark 4.5]).

The second set of conditions we present relies on the notion of purity introduced in [Reference Rosický and Tendas22], and on the main result of the same paper which classifies injectivity classes in terms of closure under certain constructs. First we need the following result:

Proposition 7.9. Assume that $\mathcal {E}$ is closed under products in $\mathcal {V}^\to $ and $\mathbb T$ be a theory consisting of sequents of the form

$$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x))\end{align*} $$

where $\varphi $ and $\psi $ are positive-primitive formulas in ${\mathbb L}_{\lambda \lambda }$ .

Then $\operatorname {\mathbf {Mod}}(\mathbb T)$ is closed in $\operatorname {\mathbf {Str}}({\mathbb L})$ under products, powers by $\mathcal {E}$ -stable objects, $\lambda $ -directed colimits, and $\lambda $ -elementary (equivalently, $(\lambda ,\mathcal {E})$ -pure) subobjects.

Proof. Following Lemma 4.8, $\operatorname {\mathbf {Mod}}(\mathbb T)$ is closed under products, powers by $\mathcal {E}$ -stable objects, and $\lambda $ -directed colimits. Closure under $\lambda $ -elementary subobjects follows from Proposition 6.4, and this coincides with closure under $(\lambda ,\mathcal {E})$ -pure ones by Proposition 6.6.

Theorem 7.10. Suppose that Assumption 6.1 and the assumptions of [Reference Rosický and Tendas22, Theorem 5.5] hold. The following are equivalent for a full subcategory $\mathcal {A}$ of $\operatorname {\mathbf {Str}}({{\mathbb L}})$ :

  1. (1) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a regular ${\mathbb L}_{\lambda \lambda }$ -theory ${\mathbb T}$ ;

  2. (2) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a theory ${\mathbb T}$ with sequents of the form

    $$ \begin{align*}(\forall x)( \varphi(x) \vdash (\exists y)\psi(x,y))\end{align*} $$
    where $\varphi $ and $\psi $ are conjunctions of atomic formulas in ${\mathbb L}_{\lambda \lambda }$ ;
  3. (3) $\mathcal {A}\cong \operatorname {\mathbf {Mod}}({\mathbb T})$ for a theory ${\mathbb T}$ with sequents of the form

    $$ \begin{align*}(\forall x)( \varphi(x) \vdash \psi(x))\end{align*} $$
    where $\varphi $ and $\psi $ are positive-primitive formulas in ${\mathbb L}_{\lambda \lambda }$ ;
  4. (4) $\mathcal {A}$ is closed under products, powers by $\mathcal {E}$ -stable objects, $\lambda $ -filtered colimits, and $\lambda $ -elementary subobjects;

  5. (5) $\mathcal {A}$ is closed under products, powers by $\mathcal {E}$ -stable objects, $\lambda $ -filtered colimits, and $(\lambda ,\mathcal {E})$ -pure subobjects;

  6. (6) $\mathcal {A}$ is a $(\lambda ,\mathcal {E})$ -injectivity class in $\operatorname {\mathbf {Str}}({{\mathbb L}})$ .

Proof. The implications $(1)\Rightarrow (2)\Rightarrow (3)$ follow by definition, $(3)\Rightarrow (4)$ follows by Proposition 7.9 above, and $(4)\Rightarrow (5)$ by Proposition 6.4. Then, $(5)\Rightarrow (6)$ is given by [Reference Rosický and Tendas22, Theorem 5.5], and finally $(6)\Rightarrow (1)$ follows from Theorem 7.6.

This corollary applies both to $\operatorname {\mathbf {Met}}$ and $\operatorname {\mathbf {Ban}}$ for the factorization system induced by the dense maps; as well as for any symmetric monoidal quasivariety $\mathcal {V}$ with the (regular epi, mono) factorization system.

Let us explain now how existential quantification is interpreted for one particular base of enrichment.

Remark 7.11. Consider $\mathcal {V}=\operatorname {\mathbf {Met}}$ and the factorization system given by the dense maps. In this example we spell out what it means for an ${{\mathbb L}}$ -structure M to satisfy a formula of the form

$$ \begin{align*}(\forall x)(\exists y)\ \psi(x,y),\end{align*} $$

with $\psi (x,y): X+Y$ a conjunction of atomic formulas. Since existential quantification is not involved in the definition of $\psi $ , we know that $\psi _M\subseteq M^X\times M^Y$ is identified by all the pairs $(a,b)$ for which $M\models \psi [a,b]$ . It follows that $((\exists y)\psi )_M$ is given by the closure of the subspace

$$ \begin{align*}\{ a\in M^X \ | \ \exists b\in M^Y\ M\models \psi[a,b] \}\subseteq M^X\end{align*} $$

under limits of Cauchy sequences. As a consequence, $M\models (\forall x)(\exists y)\ \psi (x,y)$ if and only if

$$\begin{align*}\begin{matrix}\textit{for each }a\in M^X \textit{there is a Cauchy sequence }(a_n)_{n\geq 0}\subseteq M^X\\ \textit{and }(b_n)_{n\geq 0}\subseteq M^Y \textit{(not necessarily Cauchy) such that }a=\lim_na_n\\ \textit{and }M\models \psi[a_n,b_n] \textit{for each }n. \end{matrix}\end{align*}$$

This can equivalently be expressed as follows

$$\begin{align*}\begin{matrix}\textit{for each }a\in M^X \textit{and for each }\epsilon>0 \textit{ there exist }a'\in M^X \textit{and }b'\in M^Y\\\textit{such that }d(a,a')<\epsilon \textit{ and }M\models \psi[a',b']. \end{matrix}\end{align*}$$

The same argument works in the case of $\mathcal {V}=\operatorname {\mathbf {CMet}}$ or $\mathcal {V}=\operatorname {\mathbf {Ban}}$ where the left class of the factorization system is given again by the dense maps.

Example 7.12. Consider again $\mathcal {V}=\operatorname {\mathbf {Met}}$ with the factorization system given by either the surjections or the dense maps. Let ${\mathbb I}:=[0,\infty ]$ be the positive real line with infinity included; we have two maps $i_0,i_\infty \colon 1\to {\mathbb I}$ which pick out $0$ and $\infty $ respectively. Then to give an element $p\in M^{\mathbb I}$ is the same as to give a path (of possibly length infinity) between two points in M.

We can then consider the following formula

$$ \begin{align*}(\forall (x,y):1+1) (\exists p:{\mathbb I}) (p(i_0)(x)=x\ \wedge\ p (i_\infty)(y)=y)\end{align*} $$

on the empty language over $\operatorname {\mathbf {Met}}$ .

If $\mathcal {E}$ is the class of surjections, then a metric space M satisfies the sentence above if and only if it is path connected. More interestingly, if $\mathcal {E}$ is the class of dense maps, a metric space M satisfies the sentence above if and only if

$$\begin{align*}\begin{matrix}\textit{for each }a,b\in M \textit{and for any }\epsilon>0 \textit{ there exist }a',b'\in M \textit{with }d(a,a'),d(b,b')<\epsilon\\\textit{and a path }p\colon {\mathbb I}\to M \textit{ for which }p(0)=a' \textit{and }p(\infty)=b'. \end{matrix}\end{align*}$$

A space satisfying the condition above need not be path connected; one example is given by the subspace of ${\mathbb R}^2$ given by

$$ \begin{align*}\{(x,\mathrm{sin}(1/x))\ |\ x>0 \}\cup (\{0\}\times [-1,1])\end{align*} $$

which is one of the canonical examples of a connected space which is not path connected. However, it is easy to see that this space satisfies the condition above.

Example 7.13. Let us take $\mathcal {V}=\mathbf {DGAb}$ , the monoidal category of differentially graded abelian groups, with the (regular epi, mono) factorization system. The unit I of $\mathbf {DGAb}$ is the chain complex with ${\mathbb Z}$ in degree $0$ and trivial otherwise. Let P be the chain complex with ${\mathbb Z}$ in degree $1$ and $0$ , differential $1_{\mathbb Z}$ between those, and trivial everywhere else. Then we have an inclusion $i\colon I\to P$ .

Consider now the sentence

$$ \begin{align*}(\forall x) (\exists y)\ (i(y)=x)\end{align*} $$

in the empty language, where $x:I$ and $y:P$ . It is easy to see that a chain complex A satisfies the sentence above if and only if it forms a long exact sequence (that is, if $\mathrm {Im}(d_A^{n+1})=\mathrm {Ker}(d_A^n)$ for each n).

Example 7.14. Given a small category $\mathcal {C}$ , consider the base of enrichment $\mathcal {V}=[\mathcal {C}^{\operatorname {op}},\operatorname {\mathbf {Set}}]$ with its cartesian closed structure and the (epi, mono) factorization system. Recall that, if J is a Grothendieck topology on $\mathcal {C}$ , then there is an induced notion of J-dense subobject $U\rightarrowtail V$ in $\mathcal {V}$ (see [Reference MacLane and Moerdijk16, Section V.1]). Consider the regular theory ${\mathbb T}$ given by the sentences

$$ \begin{align*}(\forall x)\ (\exists! y)\ (my=x),\end{align*} $$

in the empty language over $\mathcal {V}$ , where $m\colon A\rightarrowtail \mathcal {C}(-,C)$ is any J-dense map with representable codomain. Here the symbol $\exists !$ is interpreted as explained in Notation 4.17. Then, using [Reference MacLane and Moerdijk16, Theorem V.4.2] and the fact that sheaves are stable under powers, it is easy to see that

$$ \begin{align*}\operatorname{\mathbf{Mod}}({\mathbb T})=\mathrm{Sh}(\mathcal {C},J)\end{align*} $$

is the Grothendieck topos of sheaves over the site $(\mathcal {C},J)$ .

More generally, one could start with $\mathcal {V}$ being any Grothendieck topos endowed with the cartesian closed structure and the (epi, mono) factorization system. Then, for any Lawvere–Tierney topology j on $\mathcal {V}$ , we can express the full subcategory $\mathrm {Sh}_j\mathcal {V}$ of $\mathcal {V}$ spanned by the j-sheaves as the $\mathcal {V}$ -category of models of a regular theory.

Acknowledgments

We thank Joshua Wrigley for valuable feedback.

Funding

Both authors acknowledge the support of the Grant Agency of the Czech Republic under the grant 22-02964S. The second author also acknowledges the support of the EPSRC postdoctoral fellowship EP/X027139/1.

References

REFERENCES

Adámek, J. and Rosický, J., Locally Presentable and Accessible Categories , Cambridge University Press, Cambridge, 1994.CrossRefGoogle Scholar
Adámek, J. and Rosický, J., Approximate injectivity and smallness in metric-enriched categories . Journal of Pure and Applied Algebra , vol. 226 (2022), p. 106974.CrossRefGoogle Scholar
Bird, G.J., Limits in 2-categories of locally-presented categories, PhD thesis, University of Sydney, 1984; published as a Sydney Category Seminar Report.Google Scholar
Borceux, F., Handbook of Categorical Algebra 2 , Cambridge University Press, Cambridge, 1994.Google Scholar
Bourke, J., Lack, S., and Vokřínek, L., Adjoint functor theorems for homotopically enriched categories . Advances in Mathematics , vol. 412 (2023), p. 108812.CrossRefGoogle Scholar
Cockett, J. R. B. and Cruttwell, G. S. H., Differential structure, tangent structure, and SDG . Applied Categorical Structures , vol. 22 (2014), pp. 331417.CrossRefGoogle Scholar
Freyd, P. J. and Kelly, G. M., Categories of continuous functors, I . Journal of Pure and Applied Algebra, vol. 2 (1972), pp. 169191.CrossRefGoogle Scholar
Iovino, J., Applications of Model Theory to Functional Analysis , Dover Publication, Mineola, New York, 2014.Google Scholar
Kelly, G. M., Basic Concepts of Enriched Category Theory , Cambridge University Press, Cambridge, 1982.Google Scholar
Kelly, G. M., Structures defined by finite limits in the enriched context I . Cahiers de Topologie et Géométrie Différentielle Catégoriques , vol. 23 (1982), pp. 342.Google Scholar
Lack, S. and Rosický, J., Enriched weakness . Journal of Pure and Applied Algebra , vol. 216 (2012), pp. 8071822.CrossRefGoogle Scholar
Lack, S. and Tendas, G., Enriched regular theories . Journal of Pure and Applied Algebra , vol. 224 (2020), p. 106268.Google Scholar
Lack, S. and Tendas, G., Accessible categories with a class of limits . Journal of Pure and Applied Algebra , vol. 228 (2024), p. 107444.CrossRefGoogle Scholar
Lucyshyn-Wright, R. B. B., Enriched factorization systems . Applied Categorical Structures , vol. 29 (2014), pp. 475495.Google Scholar
Lucyshyn-Wright, R. B. B. and Parker, J., Locally bounded enriched categories . Applied Categorical Structures , vol. 38 (2022), pp. 684736.Google Scholar
MacLane, S. and Moerdijk, I., Sheaves in Geometry and Logic: A First Introduction to Topos Theory , Springer, Heidelberg and New York, 2012.Google Scholar
Pothoven, K. L., A category of Banach spaces, Master thesis, Western Michigan University, 1968.Google Scholar
Pumplün, D. and Röhrl, H., Banach spaces and totally convex spaces I . Communications in Algebra , vol. 12 (1984), pp.9531019.CrossRefGoogle Scholar
Rosický, J., Adámek, J., and Borceux, F., More on injectivity in locally presentable categories . Applied Categorical Structures , vol. 10 (2002), pp. 148161.Google Scholar
Rosický, J., Abstract tangent functors . Diagrammes , vol. 12 (1984), pp. JR1–JR11.Google Scholar
Rosický, J., Discrete equational theories . Mathematical Structures in Computer Science , vol. 34 (2024), pp. 147160.CrossRefGoogle Scholar
Rosický, J. and Tendas, G., Notions of enriched purity, Theory and Applications of Categories , 41(58), (2024), 20582104.Google Scholar
Rosický, J. and Tendas, G., Towards enriched universal algebra, preprint, 2023, arXiv:2310.11972.Google Scholar