The Essentially Equational Theory of Horn Classes

Hans–E. Porst

Dedicated to Professor Dr. Dieter Pumplün on the occasion of his retirement

Abstract

It is well known that the model categories of universal Horn theories are locally presentable, hence essentially algebraic [2]. In the special case of quasivarieties a direct translation of the implicational syntax into the essentially equational one is known [1]. Here we present a similar translation for the general case, showing at the same time that many relationally presented Horn classes are in fact (equivalent to) quasivarieties.

Mathematics Subject Classification (1991). Primary 03C07, Secondary 08C15.

Key words: Universal Horn class, quasivariety, essentially equational theory.

Introduction

The class of locally finitely presentable categories is known to comprise all complete categories of finitary (many-sorted) algebras (see [3]). There is a universal syntax by which locally finitely presentable categories can be specified, namely that of an essentially equational theory, which generalizes the classical syntax of equational classes of algebras to a specification of certain classes of partial algebras (see [2]). While it is easy to specify implicationally defined classes of algebras this way (see [1]), a canonical specification for Horn classes (which are known to be locally finitely presentable categories) by an essentially equational theory seems not to be known: The univeral representation presented in [2] might be viewed unnatural: e.g., representing POS — the category of partially ordered sets and monotone maps — this way would require ℵ_{0} sorts, whereas a 1–sorted representation is possible, as is shown in [5].

We are to provide in this note — combining ideas of [1] and [5] — an essentially equational representation of Horn classes much simpler than in [2], which moreover in many cases represents Horn classes as quasivarieties. The main idea is to introduce, for each relational symbol provided by the signature under consideration, a new sort and a family of operations corresponding to the respective projections; this enables us, in a second step, to represent (relational) implications in terms of (partial) operations and equations. For a related approach see [4].

Preliminaries

Language and notation are mainly as in [2]. To make this note as selfcontained as possible we briefly explain the basic notions.

Products of (finite) families of sets or maps are denoted by ∏_{i=1}^{n} A_{i} or A_{1} ×…×A_{n}

(respectively ∏_{i=1}^{n} f_{i} or f_{1} ×…×f_{n}) according to convenience; the product projection

onto the i-th component of a (subset of a) product is denoted by π_{i}, with superscripts

referring to the particular product if necessary. The map B ⟶ ∏_{i=1}^{n} A_{i} induced by

a family of maps (g_{i}: B ⟶ A_{i})_{i=1...n}, i.e., the map g with π_{i} ∘ g = g_{i} for each i is denoted by ⟨g_{i}⟩.

Let Σ = Σ_{op} ˙∪ Σ_{rel} be an S–sorted finitary signature, i.e., S is a set of sorts, Σ_{op} is set of operational symbols, Σ_{rel} is a set of relational symbols, and for each symbol ω ∈ Σ there is given an arity arω = (s_{1}, …, s_{n}, s_{0}) ∈ S^{n+1} (for some n ∈ ℕ) . In view of the role the arities are to play we will use more suggestive notions for them as follows:

• for σ ∈ Σ_{op} we write s_{1} × … × s_{n} → s_{0} instead of (s_{1}, …, s_{n}, s_{0}).

• for σ ∈ Σ_{rel} we write s_{1} × … × s_{n} × s_{0} instead of (s_{1}, …, s_{n}, s_{0}).

A Σ-structure then is a triple A = ((A_{s})_{s∈S}, (σ^{A})_{σ∈Σ_{op}}, (R^{A})_{R∈Σ_{rel}}) where (A_{s})_{s∈S} is a family of S-indexed sets, σ^{A}: A_{s_{1}} × … × A_{s_{n}} → A_{s_{0}} is a map for each σ ∈ Σ_{op} with arσ = s_{1} × … × s_{n} → s_{0}, and R^{A} ⊂ A_{s_{1}} × … × A_{s_{n}} × A_{s_{0}} is a subset for each R ∈ Σ_{rel} with arR = s_{1} × … × s_{n} × s_{0}. A morphism of Σ-structures f: A → B is an S-indexed family of maps (f_{s}: A_{s} → B_{s})_{s∈S} satisfying the conditions

• σ^{B}∘(f_{s_{1}} × … × f_{s_{n}}) = f_{s_{0}}∘σ^{A} for each σ ∈ Σ_{op} with arσ = s_{1} × … × s_{n} → s_{0},

• f_{s_{1}} × … × f_{s_{n}}[R^{A}] ⊂ R^{B} for each R ∈ Σ_{rel} with arR = s_{1} × … × s_{n} × s_{0}.

This defines the category StrΣ of Σ-structures which – by means of the obvious underlying functor StrΣ ⟶ Set^{S} – is a concrete category over Set^{S}, the S-fold power of the category of sets and mappings.

The signature Σ is called finite provided both, S and Σ, are finite sets. As usual Σ is called a signature of algebras if Σ_{rel} is empty; in this case Σ-structures are simply denoted as pairs ((A_{s})_{s∈S}, (σ^{A})_{σ∈Σ_{op}}).

The following particular types of subcategories of categories of the form StrΣ are of special interest:

Horn classes: Let there be given a set I of Σ–implications

α_{1} ∧ α_{2} ∧ … ∧ α_{n} ⟹ β

where n ∈ ℕ and α_{i} and β are atomic Σ–formulas (i.e., either Σ_{op}-equations, or formulas R(t_{1}, …, t_{m}) where R ∈ Σ_{rel} is an m–ary relational symbol and t_{1}, …, t_{m} are terms of the corresponding sorts). The full subcategory Mod(Σ, I) of StrΣ spanned by all Σ–structures satisfying the implications in I is then called a (universal) Horn class. If, for each implication in I, the conclusion β is in fact an equation, we call the Horn class quasivarietal.

In case Σ_{rel} = ∅ the category Mod(Σ, I) is called a quasivariety. The category POS of partially ordered sets is an example of a Horn class, which is not a quasivariety. Horn classes are locally finitely presentable categories (see [2]).

Categories of partial algebras: Denote by PAlgΣ the full subcategory of StrΣ consisting of those Σ-structures A for which each relation R^{A} (R ∈ Σ_{rel}, arR = (s_{1}, …, s_{n}, s_{0})) satisfies

(a_{1}, …, a_{n}, a_{0}), (a_{1}, …, a_{n}, b_{0}) ∈ R^{A} ⟹ a_{0} = b_{0}.

In other words, for any A in PAlgΣ each relation R^{A} with arity (s_{1}, …, s_{n}, s_{0}) “is” a partial map from some subset domR^{A} ⊂ A_{s_{1}} × … × A_{s_{n}} into A_{s_{0}}.

Considering categories of the form PAlgΣ we might speak of partial operational symbols instead of relational symbols and denote their arities the same way as for (total) operational symbols; we also might write Σ_{p} instead of Σ_{rel} and Σ_{t} instead of Σ_{op} in this case, and then call Σ a signature of partial algebras.

Essentially equational (essentially algebraic) categories: By an essentially equational theory (Ω, def, E) with set of sorts S we mean a S–sorted finitary signature Ω = Ω_{t} ˙∪ Ω_{p} of partial algebras together with finite sets defω of Ω_{t}–equations for each ω ∈ Ω_{p} (the domain conditions of ω), where for arω = s_{1} × … × s_{n} → s_{0} the elements of defω are equations in the S-sorted variables x_{s_{1}}, …, x_{s_{n}}, and a set E of Ω–equations (the identities of the theory). The theory is called finite if S and Ω are finite sets.

A partial Ω–algebra A is called a model of this theory iff

(i) the operations ω^{A} are total for each ω ∈ Ω_{t};

(ii) for ω ∈ Ω_{p} with arω = s_{1} × … × s_{n} → s_{0} and (a_{1}, …, a_{n}) ∈ A_{s_{1}} × … × A_{s_{n}} one has (a_{1}, …, a_{n}) ∈ domω^{A} iff t^{A}(a_{1}, …, a_{n}) = t′^{A}(a_{1}, …, a_{n}) for all equations t ∼ t′ ∈ defω.

(iii) A satisfies the identities of E^{1}.

1Satisfaction here is meant in the weak sense: if both sides of the equation are defined then they are equal.

These models form the full subcategory Mod(Ω, def, E) of PAlgΩ (which thus is a concrete category over Set^{T}).

Categories of the form Mod(Ω, def, E) for essentially equational theories (Ω, def, E) are called essentially algebraic (or essentially equational) categories. It is shown in [2] that the locally finitely presentable categories are (up to equivalence of categories) precisely the essentially equational categories.

A paradigmatic example of a (1-sorted) essentially equational category ist the category Cat of small categories and functors: the total operations are — besides the identities as constants — domain and codomain, the only partial (binary) operation is composition and defcomposition consists of the single equation domain (x) = codomain (y). Cat is not (equivalent to) a Horn class.

Each quasivariety has a canonical representation by an essentially equational theory as follows (see [1]): add to the given siganture, for each implication

ϱ_{1} ∼ τ_{1} ∧ … ∧ ϱ_{n} ∼ τ_{n} ⟹ π ∼ τ,

one partial operation ω with domain condition defω = {ϱ_{i} ∼ τ_{i} | i = 1, …, n} together with the equations ω ∼ π and ω ∼ τ.

Results

For a given S–sorted finitary signature Σ = Σ_{op}∪Σ_{rel} we define an S^{∗}–sorted finitary signature of algebras Ω^{Σ} as follows:

• S^{∗} = S ˙∪{s_{R} | R ∈ Σ_{rel}} is the set of sorts.

• Ω_{op}^{Σ} = Σ_{op} ˙∪ ⋃{Σ_{R} | R ∈ Σ_{rel}} is its set of operational symbols, where, for R ∈ Σ_{rel} of arity s_{1} × … × s_{n}, the set Σ_{R} consists of n = n(R) (unary) operational symbols ^{R}π_{i} (i = 1, …, n) with arities s_{R} → s_{i}; the arity of σ ∈ Σ_{op} is the one given by the signature Σ.

Note that Ω^{Σ} is finite provided Σ is finite.

Proposition 1 For every S–sorted finitary signature Σ there exist a finitary S^{∗}– sorted signature of algebras Ω^{Σ}, a set I^{Σ} of Ω^{Σ}–implications, and functors

StrΣ ⟶^{G^{Σ}} Mod(Ω^{Σ}, I^{Σ}) ⟶^{F^{Σ}} Str Σ

such that F^{Σ} ∘ G^{Σ} = 1 and G^{Σ} ∘ F^{Σ} ≃ 1.

If the signature Σ is finite, so is the signature Ω^{Σ} and also the set of implications I^{Σ}.

The above proposition — being only a slight generalization of [2, 3.20] — is included here, as well as its proof, because it serves as a basis for the (proofs of) the following results.

Proposition 2 Let Σ be an S–sorted finitary signature and Mod(Σ, J) ⊂ StrΣ a quasivarietal Horn class. Then there exists a set I^{J} of Ω^{Σ}–implications (of the same cardinality as J) such that G^{Σ} and F^{Σ} can be restricted to an equivalence between Mod(Σ, J) and the S^{∗}–sorted quasivariety Mod(Ω^{Σ}, I^{Σ} ∪ I^{J}).

Proposition 3 Let Σ be an S–sorted finitary signature and H = Mod(Σ, J) ⊂ StrΣ an arbitrary universal Horn class. Then there exists an essentially equational theory (Ω^{H}, def, E^{H}) with set of sorts S^{∗} such that H and Mod(Ω^{H}, def, E^{H}) are equivalent.

If Σ is a finite signature and the set J of implications is finite, then (Ω^{H}, def, E^{H}) is a finite theory.

Proofs

Proof of Proposition 1. For Σ = Σ_{op} ∪ Σ_{rel} with set of sorts S we have S^{∗} = S ˙∪ Σ_{rel} and Ω^{Σ} = Σ_{op} ˙∪ ⋃{Σ_{R} | R ∈ Σ_{rel}}. Define I^{Σ} as

I^{Σ} = { ^{R}π_{1}x ∼ ^{R}π_{1}y ∧ … ∧ ^{R}π_{n}x ∼ ^{R}π_{n}y ⟹ x ∼ y | R ∈ Σ_{rel}}

Given a Σ–structure

A = ((A_{s})_{s∈S}, (σ^{A})_{σ∈Σ_{op}}, (R^{A})_{R∈Σ_{rel}})

define

G^{Σ}A = ((Ā_{t})_{t∈S^{∗}}, (σĀ)_{σ∈Σ_{op}}, ( ^{R}πĀ ; i)_{^{R}π_{i}∈Σ_{R}, R∈Σ_{rel}})

by

• Ā_{t}: = \{ \begin{matrix}A_{s} & if & t = s ∈ S \\ R^{A} & if & t = s_{R}, R ∈ Σ_{rel} \end{matrix}

• σĀ: = σ^{A}

• ^{R}πĀ ; i: = ∏_{i=1}^{n(R)} A_{s_{i}} ⊃ R^{A} ⟶^{π_{i}} A_{s_{i}} i.e., ^{R}πĀ ; i is the (restricted) product projection.

G^{Σ}A then obviously satisfies all implications in I^{Σ}. G^{Σ} becomes a functor if one defines, for a StrΣ–morphism h = (h_{s})_{s∈S}: A ⟶ B, G^{Σ}h = (h̄_{t}: Ā_{t} ⟶ B̄_{t})_{t∈S^{∗}} by

h̄_{t} = \{ \begin{matrix}h_{s} & : A_{s} ⟶ B_{s} & if & t = s ∈ S \\ ∏_{i=1}^{n(R)} h_{s_{i}} & : R^{A} ⟶ R^{B} & if & t = s_{R}, R ∈ Σ_{rel}^{2} \end{matrix}

2here, clearly, h̄_{s_{R}} is meant to be ∏ h_{s_{i}} restricted and corestricted to R^{A} and R^{B} respectively.

Now define, for any (Ω^{Σ}, I^{Σ})–model

A = ((A_{t})_{t∈S^{∗}}, (σ^{A})_{σ∈Ω_{op}^{Σ}}),

the Σ–model

F^{Σ}A = ((Ã_{s})_{s∈S}, (σÃ)_{σ∈Σ_{op}}, (RÃ)_{R∈Σ_{rel}})

by • Ã_{s}: = A_{s},

• σÃ: = σ_{A},

• RÃ: = im ⟨^{R}π_{i}^{A}⟩ i.e., RÃ is the image of the map ⟨^{R}π_{i}^{A}⟩: A_{s_{R}} ⟶ ∏_{i=1}^{n(R)} A_{s_{i}}.

F^{Σ} becomes a functor if we define

F^{Σ}((A_{t} ⟶^{h_{t}} B_{t})_{t∈S^{∗}}) = (A_{s} ⟶^{h_{s}} B_{s})_{s∈S}.

It is obvious that the equation F^{Σ}∘G^{Σ} = 1 holds. Also for A = ((A_{t})_{t∈S^{∗}}, (σ^{A})_{σ∈Ω^{Σ}}) and G^{Σ} ∘ F^{Σ}A = ((Ã- _{t})_{t∈S^{∗}}), ((σ ^{¯Ã})_{σ∈Ω^{Σ}}) one obviously has

• Ã-_{s} = A_{s} for each s ∈ S

• σ ¯Ã = σ^{A} for each σ ∈ Σ_{op}

For R ∈ Σ_{rel} we have Ã-_{s_{R}} = RÃ = im⟨(^{R}π_{i}^{A})_{i}⟩. Since A satisfies the implications of I^{Σ}, the map ⟨( ^{R}π_{i}^{A})_{i}⟩ is monic, hence a bijection χ_{R}^{A}: A_{s_{R}} ⟶^{∼} RÃ. Similarly, for h = (h_{t})_{t∈S^{∗}}: A ⟶ B in Mod(Ω^{Σ}, I^{Σ}) and G^{Σ} ∘ F^{Σ}h = (¯h̃)_{t∈S^{∗}} one has ¯ h̃_{s} = h_{s} for each s ∈ S. For R ∈ Σ_{rel} the map ¯ h̃_{S_{R}}: RÃ ⟶ RB̃ is the (co/restriction) of ∏_{i=1}^{n(R)} h_{s_{i}}. Hence, in the following diagram all cells commute.

\xymatrix{A_{s_{R}} \ar[d]_{χ_{R}^{A}} \ar[ddd]_{^{R}π_{i}^{A}} \ar[r]^{h_{s_{R}}} & B_{s_{R}} \ar[d]^{χ_{R}^{B}} \ar[ddd]^{^{R}π_{i}^{B}} \\ RÃ \ar[r]^{_{¯h̃_{R}}} \ar[d] & RB̃ \ar[d] \\ ∏ A_{s_{i}} \ar[d]_{π_{i}} \ar[r]^{∏ h_{s_{i}}} & ∏ B_{s_{i}} \ar[d]^{π_{i}} \\ A_{s_{i}} \ar[r]_{h_{s_{i}}} & B_{s_{i}}}

Thus, the S^{∗}–sorted maps χ_{t}^{A}: A_{t} ⟶ ¯Ã_{t} with

χ_{t}^{A} = \{ \begin{matrix}1_{A_{s}} & if & t = s ∈ S \\ χ_{R}^{A} & if & t = s_{R}, R ∈ Σ_{rel} \end{matrix}

are isomorphisms A ⟶ G^{Σ}F^{Σ}A, natural in A. ◇

Lemma Let Σ be a S–sorted finitary signature and α = Q(t_{1}, … t_{n}) an atomic Σ–formula with Q a relational symbol of arity s_{1} × … × s_{n}. Let E_{α} be the set of Ω^{Σ}–equations

E_{α} = { ^{Q}π_{1} ∼ t_{1}, …,^{Q} π_{n} ∼ t_{n}} .

Then the following holds:

(i) If ā = (a_{1}, …, a_{m}) is an assignment to variables in the Σ–structure A such that (t_{1}^{A}(ā), …, t_{n}^{A}(ā)) ∈ Q^{A}, then there exists an assignment ā^{∗} = (b, a_{1}, …, a_{m}) in the (Ω^{Σ}, I^{Σ})–model G^{Σ}A fulfilling all equations in E_{α}.

(ii) Let b̄ = (b, a_{1}, …, a_{m}) be an assignment to variables in the (Ω^{Σ}, I^{Σ})–model A such that b̄ fulfills all equations in E_{α}; then (t_{1}^{F^{Σ}A}(b̄^{•}), …, t_{n}^{F^{Σ}A}(b̄^{•})) ∈ Q^{F^{Σ}A} for the assignment b̄^{•} = (a_{1}, …, a_{m}) in the in the Σ–structure F^{Σ}A.

Proof x_{1}, …, x_{m} denote the S–sorted variables needed by t_{1}, …, t_{n}, x_{i} of sort s_{i}.

Let A = ((A_{s}), (σ^{A})_{σ}, (R^{A})_{R}) be a Σ–structure and ā = (a_{1}, …, a_{m}) with a_{i} ∈ A_{s_{i}} an assignment to the variables x_{1}, …, x_{m}, such that (t_{i}^{A}(ā), …, t_{n}^{A}(ā) ∈ Q^{A}. Then ā^{∗} = (b, a_{1}, …, a_{n}) with b = (t_{1}(ā), …, t_{n}(ā)) is an assignment to the S^{∗}–sorted variables (x, x_{1}, …, x_{m}) with x of sort s_{Q} in the Ω^{Σ}–model G^{Σ}A. To prove that ā^{∗} fulfills all equations in E_{α} now is trivial.

Conversely, if b̄ = (b, a_{1}, …, a_{m}) is an assignment to the S^{∗}–sorted variables (x, x_{1}, …, x_{m}) with x of sort s_{Q} in the Mod(Ω^{Σ}, I^{Σ})–model A = ((A_{t})_{t}, (σ^{A})_{σ}) fulfilling all equations in E_{α} a straightforward calculation shows that for the assignment b̄^{•} = (a_{1}, …, a_{m}) to the S–sorted variables x_{1}, …, x_{m} in the Σ–structure F^{Σ}A one has (t_{1}^{F^{Σ}A}(b̄^{•}), …, t_{n}^{F^{Σ}A}(b̄^{•})) ∈ Q^{F^{Σ}A}. ◇

Proof of Proposition 2. For each implication

J: α_{1} ∧ … ∧ α_{k} ⟹ s ∼ t

we consider the sets E_{α_{i}} of Ω^{Σ}–equations as in the Lemma where applicable. If α_{i} = (s_{i} ∼ t_{i}) is an equation we define E_{α_{i}} to be {s_{i} ∼ t_{i}}. By e_{i} we denote the conjunction of the equations of E_{α_{i}}, i.e.,

e_{i} = \{ \begin{matrix}( ^{R_{i}}π_{1} ∼ t_{1}^{i}) ∧ … ∧ ( ^{R_{i}}π_{n_{i}} ∼ t_{n_{i}}^{i}) & if & α_{i} = R_{i}(t_{1}^{i}, … t_{n_{i}}^{i}) \\ s_{i} ∼ t_{i} & if & α_{i} = (s_{i} ∼ t_{i}) \end{matrix}

Let now J̄ be the implication

J̄: e_{1} ∧ e_{2} ∧ … ∧ e_{k} ⟹ s ∼ t

and I^{J} the set of all implications J̄ for J ∈ J. It remains to show that G^{Σ} maps H = Mod(Σ, J) into Mod(Ω^{Σ}, I^{Σ} ∪I^{J}) and that F^{Σ} maps this category back into H.

Let A = ((A_{s})_{s}, (σ^{A})_{σ}, (R^{A})_{R}) be in H. It suffices to show that G^{Σ}A satisfies all implications of the form J̄. Let now b̄ be an assignment to the variables needed for J̄ in G^{Σ}A satisfying the premis J̄. Then b̄ satisfies all equations in E_{α_{i}} for each i = 1, …, k. By (ii) of the Lemma there results an assignment b̄^{•} in F^{Σ}G^{Σ}A = A such that each atomic formula α_{i} is satisfied by b̄^{•}. Since J holds in A we conclude s^{A}(b̄^{•}) = t^{A}(b̄^{•}), hence^{G^{Σ}A}s(b̄) = ^{G^{Σ}A}t(b̄), since b̄ and b̄^{•} differ only in (not) assigning values to variables of the sorts s_{R_{i}} which don’t occur in s and t respectively.

Conversely, let A = ((A_{t})_{t}, (σ^{A})_{σ}) be in Mod(Ω^{Σ}, I^{Σ} ∪ I^{J}) and ā an assignment to the variables needed in J ∈ J in the Σ–structure F^{Σ}A, such that each atomic formula α_{i} occuring in the premis of J is satisfied by ā. By (i) of the Lemma there exists an assignment ā^{∗} in G^{Σ}F^{Σ}A fulfilling the equations in E_{α_{i}} for all i. Since G^{Σ}F^{Σ}A and A are isomorphic by Proposition 1 and A satisfies the implications in I^{J} so does G^{Σ}F^{Σ}A; hence we conclude

s^{G^{Σ}F^{Σ}A}(ā^{∗}) = t^{G^{Σ}F^{Σ}A}(ā^{∗}), thus s^{F^{Σ}A}(ā) = t^{F^{Σ}A}(ā). ◇

Before considering the general case of an arbitrary Horn class H ⊂ StrΣ we recall from the introduction the description of the quasivariety Mod(Ω^{Σ}, I^{Σ}) by means of an essentially equational theory: (Ω̃^{Σ}, def, E^{Σ}) is the essentially equational theory with

• S^{∗} as set of sorts,

• Ω̃_{t}^{Σ} = Ω_{op}^{Σ}

• Ω̃_{p}^{Σ} = {R̃ | R ∈ Σ_{rel}}, where for each R ∈ Σ_{rel} of arity s_{1} × … × s_{n} the corresponding R̃ is considered as a (binary) operational symbol of arity s_{R} × s_{R} → s_{R} with domain condition

defR̃ = { ^{R}π_{i}x ∼ ^{R}π_{i}y | i = 1, …, n} .

• E^{Σ} = ⋃_{R∈Σ_{rel}} E_{R} with E_{R} = {R̃(x, y) ∼ x, R̃(x, y) ∼ y}

It is well known (and easy to see) that the obvious forgetful functor

Mod(Ω̃^{Σ}, def, E^{Σ}) ⟶ Mod(Ω^{Σ})

yields an isomorphism

Mod(Ω̃^{Σ}, def, E^{Σ}) ⟶ Mod(Ω^{Σ}, I^{Σ}).

Proof of Proposition 3. We continue as in the preceding remark and enlarge the theory (Ω̃^{Σ}, def, E^{Σ}) to (Ω^{H}, def, E^{H}) as follows:

• Ω_{t}^{H} : = Ω̃_{t}^{Σ} = Ω_{op}^{Σ}

• Ω_{p}^{H} : = Ω̃_{p}^{Σ} ˙∪ {J̃ | J ∈ J } = Σ_{rel} ˙∪ {J̃ | J ∈ J } where for each implication

J: α_{1} ∧ … ∧ α_{k} ⟹ β

in J (with α_{i} = R_{i}(t_{1}^{i}, …, t_{n_{i}}^{i}), β = Q(t_{1}, …, t_{m}) and needed variables x_{1}, …, x_{l} of sorts s_{1}, …, s_{l} ∈ S) J̃ is a partial operational symbol with arity

s_{R_{1}} × … × s_{R_{k}} × s_{1} × … × s_{l} → s_{Q}^{3}

with domain condition defJ̃ = ⋃_{i=1}^{k} E_{α_{i}},

• E^{H} = E^{Σ} ∪ E^{J} with E^{J} : = ⋃_{J∈J} { ^{Q}π_{i}J̃ ∼ t_{i} | i = 1, …, m}.

Observe first that the obvious forgetful functor

V : Mod(Ω^{H}, def, E^{H}) ⟶ Mod(Ω̃^{Σ}, def, E^{Σ})

is full: if h = (h_{t})_{t}: V A ⟶ V B is a homomorphism in Mod(Ω̃^{Σ}, E^{Σ}) and J ∈ J it is to be shown that, for each ā = (b_{1}, … b_{k}, a_{1}, …, a_{l}) fulfilling all equations in defJ̃ in the algebra A, h(ā) fulfills these equations in B and also the homomorphism condition

h_{Q} ∘ J̃^{A}(ā) = J̃^{B} ∘ h_{s_{R_{1}}} × … × h_{s_{R_{k}}} × h_{s_{1}} × … × h_{s_{l}}(ā) = J̃^{B}h(ā).

To prove this, consider ā = (b_{1}, …, b_{k}, a_{1}, …, a_{l}) ∈ dom J̃^{A} with b_{i} of sort s_{R_{i}}, a_{j} of sort s_{j}. ā ∈ dom J̃^{A} implies b_{i} = ^{R_{i}}π_{j_{i}}^{A}(ā) = (t_{j_{i}}^{i})^{A}(ā) for all i, j_{i}; since h is a morphism in Mod(Ω^{Σ}, I^{Σ}) one has

h_{s_{R_{i}}}(t_{j_{i}}^{i})^{A}(ā) = (t_{j_{i}}^{i})^{B}(h(ā)) for all i, j_{i},

and therefore

R_{i}π_{j_{i}}^{B}(h(ā)) = ^{R_{i}}π_{j_{i}}^{B}((h_{s_{R_{i}}}(b_{i})) = (t_{j_{i}}^{i})^{B}(h(ā)),

thus, h(ā) ∈ domJ̃^{B}. Now, for ā ∈ domJ̃^{A}, one concludes for all terms t_{i} of sorts s′_{i} occuring in the conclusion β:

Qπ_{i}^{B}J̃^{B}(h(ā)) = t_{i}^{B}(h(ā))
= h_{s′_{i}}(t_{i}^{A}(ā))
= h_{s′_{i}}( ^{Q}π_{i}^{A}J̃^{A}(ā))
= ^{Q}π_{i}^{B}h_{Q}(J̃^{A}(ā))

3omit here s_{R_{i}} if α_{i} is of the form t_{1} ∼ t_{2}

Since V B satisfies the implications in I^{Σ}, h is a homomorphism.

Next, we lift G^{Σ} and F^{Σ} along V to obtain functors G and F such that the diagram

\xymatrix{Mod(Σ, J) \ar[d] \ar[r]^{G} & Mod(Ω^{H}, def, E^{H}) \ar[d]^{V} \ar[r]^{F} & Mod(Σ, J) \ar[d] \\ StrΣ \ar[r]_{G^{Σ}} & Mod(Ω^{Σ}, I^{Σ}) \ar[r]_{F^{Σ}} & StrΣ}

commutes, which immediately yields F ∘ G = 1 and, since V is full and faithful, also G ∘ F ≃ 1.

Let A = ((A_{s})_{s}, (σ^{A})_{σ}, (R^{A})_{R}) satisfy all implications J ∈ J. Consider

G^{Σ}A = ((Ā_{t}), (σ̄^{A})_{σ∈Ω_{t}^{Σ}}, (R̃^{A})_{R∈Σ_{rel}})

(we identify, for the sake of simplicity, Mod(Ω̃^{Σ}, def, E^{Σ}) and Mod(Ω^{Σ}, I^{Σ})). Define GA: = ((Ā_{t}), (σ̄^{A})_{σ∈Ω_{t}^{Σ}}, (R̃^{A})_{R∈Σ_{rel}}, (J̃^{A})_{J∈J} ), where for

J: R_{1}(t_{1}^{1}, …, t_{n_{1}}^{1}) ∧ … ∧ R_{k}(t_{1}^{k}, …, t_{n_{k}}^{k}) ⟹ Q(t_{1}, …, t_{m}) (*)

in J with S–sorted variables x_{1}, … x_{l} of sorts s_{1}, … s_{l} needed for the t_{j_{i}}^{j}, t_{i}, the partial operation

R_{1}^{A} × … × R_{k}^{A} × ∏_{i=1}^{l} A_{s_{i}} ⊃ domJ̃^{A} ⟶^{J̃^{A}} Q^{A}

with

domJ̃^{A} = {(b_{1}, …, b_{k}, ā) | b_{j} ∈ R_{j}^{A}, ā ∈ ∏_{i=1}^{l} A_{s_{i}}, b_{j} = (t_{1}^{j}(ā), …, t_{n_{j}}^{j}(ā))}

is defined by

J̃^{A}(b_{1}, …, b_{k}, ā) = (t_{1}(ā), …, t_{m}(ā))

Then any (b_{1}, …, b_{k}, ā) ∈ ∏_{j=1}^{k} R_{j}^{A} × ∏_{i=1}^{l} A_{s_{i}} (with b_{j} = (b_{1}^{j}, …, b_{n_{j}}^{j})) satisfies all

equations in defJ̃ iff, for all j, i_{j}, the equation b_{i_{j}}^{j} = ^{R_{j}}π_{i_{j}}^{A}(b_{j}) = (t_{ij}^{j})^{A}(ā) holds, i.e., iff (b_{1}, …, b_{k}ā) ∈ domJ̃^{A}, and, if so, J̃^{A}(b_{1}, …, b_{k}, ā) ∈ Q^{A} since A satisfies the implication J.

GA satisfies the identities of E^{J}, hence of E^{H}, since for each (b_{1}, …, b_{k}, ā) as above one has

\begin{aligned}^{Q}π_{i}^{A}J̃^{A}(b_{1}, …, b_{k}, ā) & = & ^{Q}π_{i}(t_{1}^{A}(ā), …, t_{m}^{A}(ā)) \\ & = & t_{i}^{A}(ā) = t_{i}^{A}(b_{1}, …, b_{k}, ā). \end{aligned}

Since V is full we can define Gh = G^{Σ}h for morphisms h in Mod(Σ, J).

In order to define F we only need to show that, for each A in Mod(Ω^{H}, def, E^{H}), A = ((A_{t})_{t}, (σ^{A})_{σ}, (R̃^{A})_{R}, (J̃^{A})_{J}), the Σ-structure F^{Σ}V A = ((Ã_{s})_{s}, (σÃ)_{σ}, (RÃ)_{R}) satisfies all implications J ∈ J. Hence let J ∈ J be as in (*) and ā an assignment to the variables x_{1}, …, x_{l} in the algebra F^{Σ}V A such that for j = 1, …, k

b̃_{j}: = ((t_{1}^{j})Ã(ā), …, (t_{n_{j}}^{j})Ã(ā)) ∈ RÃ ; j = im⟨ ^{R_{j}}π_{i}^{A}⟩.

Then there exist uniquely determined elements (recall that the maps ⟨ ^{R_{j}}π_{i}^{A}⟩ are monic) b_{j} ∈ R_{j}^{A} (j = 1, …, k) with

R_{j}π_{i_{j}}^{A}(b_{j}) = (t_{i_{j}}^{j})^{A}(ā) for all j, i_{j}.

Since A is an (Ω^{H}, def, E^{H})–model this means in particular: (b_{1}, …, b_{k}, ā) ∈ domJ̃^{A}, J̃^{A}(b_{1}, …, b_{k}, ā) ∈ Q^{A}, and^{Q}π_{i}^{A}J̃^{A}(b_{1}, …, b_{k}, ā) = t_{i}^{A}(ā) for i = 1, …, m. It follows

(tÃ ; 1(ā), …, tÃ ; m(ā)) = (t_{1}^{A}(ā), …, t_{m}^{A}(ā)) = ⟨ ^{Q}π_{i}^{A}⟩(J̃^{A}(b_{1}, …, b_{k}, ā)) ∈ QÃ. ◇

References

[1] J. Adámek, H. Herrlich, and J. Rosický. Essentially equational categories. Cahiers Topol. Géom. Différentielles Catégoriques, 24:175–192.

[2] J. Adámek and J. Rosicky. Locally presentable and accessible categories. Cambridge, 1994.

[3] M. Makkai and R. Paré. Accessible Categories. Contemp. Math., volume 104. Amer. Math. Soc., Providence R.I., 1989.

[4] T. Mossakowski. Equivalences among various logical framework of partial algebras. In Lecture Notes in Computer Science, volume 1092, pages 403–433, 1996.

[5] H. -E. Porst. The algebraic theory of order. Appl. Categorical Structures, 1:423– 440, 1993.

Department of Mathematics, University of Bremen, 28359 Bremen, Germany

porst@math.uni-bremen.de