Theory and Applications of Categories, Vol. 12, No. 7, 2004, pp. 248–261.

CHANGE OF BASE FOR RELATIONAL VARIABLE SETS

SUSAN NIEFIELD

Abstract. Following [5], a relational variable set on a category B is a lax functor B → Rel, where Rel is the category of sets and relations. Change-of-base functors and their adjoints are considered for certain categories of relational variable sets and applied to construct the simplification of a dynamic set (in the sense of [11]).

1. Introduction

A relational variable set on a category B is a lax functor B → Rel, where Rel is the locally partially-ordered 2-category of sets and relations. Also called relational presheaves [8], specification structures [1], and dynamic sets [11], these lax functors have played a role in the study of modal and basic predicate logic [4, 5], concurrency [1], automata [8], and spatio-temporal databases [11].

For a category Rel^{B} of relational variable sets and a functor p: E → B, we consider adjoints to the change-of-base functor p^{∗}: Rel^{B} → Rel^{E}. We will see that p^{∗} always has a left adjoint Σ_{p}, while the existence of a right adjoint Π_{p} is related to the exponentiability of p in the category Cat of small categories and functors.

In “Powerful functors” [12], Street describes exponentiability in Cat via an equivalence (due to Bénabou) between the slice 2-category Cat/B and a 2-category of normal lax functors m: B^{op} → Mod, where Mod denotes the bicategory whose objects are small categories and the hom category Mod(A, B) is the functor category Set^{B^{op}×A}, and a normal lax functor strictly preserves identities. In particular, p: E → B is exponentiable if and only if the corresponding m_{E}: B^{op} → Mod is a pseudofunctor, and the latter readily translates into the Giraud-Conduché [6, 3] factorization lifting condition for exponentiability in Cat.

A modification of Bénabou’s result yields an equivalence between Rel^{B} and the category Cat_{f}/B of faithful functors over B. It turns out that a faithful functor p: E → B is exponentiable in Cat_{f}/B if and only if the corresponding relational variable set B → Rel is a non-unitary (i.e., not necessarily identity preserving) functor, or equivalently a certain weak factorization lifting property (WFLP) holds. Thus, when p: E → B is faithful, using the general relationship between exponentiability of p and the existence of Π_{p}, it follows that Π_{p}: Rel^{E} → Rel^{B} exists if and only if p satisfies WFLP, and this generalizes to the case when p is not assumed to be faithful.

Received by the editors 2003-08-14 and, in revised form, 2004-03-22.

Transmitted by Walter Tholen. Published on 2004-03-31.

2000 Mathematics Subject Classification: 18A40, 08A02, 18F20, 18A22.

Key words and phrases: relational variable set, specification structure, dynamic set, relational presheaf, change of base, exponentiable.

\begin{matrix}c \\ ◯ \end{matrix} Susan Niefield, 2004. Permission to copy for private use granted.

We begin with the introduction of the category Rel^{B} of relational variable sets and morphisms, and its equivalence to Cat_{f}/B. In §4, we consider adjoints to the changeof-base functor p^{∗}: Rel^{B} → Rel^{E}, and their relationship to the exponentiability of p. We conclude, in §5, with an application to the construction of the simplification of a dynamic set with respect to a change in time domain (in the sense of [11]).

2. Relational Variable Sets

Let Rel denote the locally partially-ordered 2-category of sets and relations, i.e., Rel(X, Y) is the poset of relations R ⊆ X×Y, with the identity morphism on X given by the diagonal Δ ⊆ X × X and composition by the usual relation composites. To distinguish relations from functions, elements of Rel(X, Y) will be denoted by R: X−↦ Y. The composite of R: X−↦ Y and S: Y −↦ Z will be written S ∘ R, and abbreviated as SR.

A relational variable set or Rel-set on a category B consists of a set X_{b}, for every object b of B, and a relation X_{β}: X_{b}−↦X_{b′}, for every morphism β: b → b′ of B, satisfying

(RS1) Δ_{X_{b}} ⊆ X_{id_{b}}

(RS2) X_{β′}X_{β} ⊆ X_{β′β}

for all objects b and for all morphisms β: b → b′ and β′: b′ → b′′ of B. Writing x →_{β} x′ for the infix form of (x, x′) ∈ X_{β}, and x →_{b} x′ when β is the identity morphism on b, these conditions become

(RS1*) x →_{b} x, for all x ∈ X_{b}

(RS2*) x →_{β} x′, x′ →_{β′} x′′ ⇒ x →_{β′β} x′′

Note that a Rel-set is just a lax functor or morphism of bicategories, in the sense of [7] or [2], respectively. Of course, X is a functor if and only if the containments in (RS1) and (RS2) are equalities.

An example (in the spirit of [11]) of a Rel-set as a model of a data base changing over time is given by

[figure: W; B_{1}; B_{2}; N; B; N; W; B; N_{2}; N_{1}; t_{1}; t_{2}; t_{3}]

Here, the objects of the category t_{1} → t_{2} → t_{3} are time values (perhaps, certain years), the elements of X_{t} represent daily flights to three airports (say, Newark, Boston, and Washington) with subscripts used to indicate multiple flights.

Among the examples from Logics for Concurrency [1] is the Rel-set on B = Rel with X_{b} = P(b) = Rel(1, b), and S →_{R} T whenever RS ⊆ T. Note that this example can be generalized to any bicategory B, where 1 is replaced by any fixed object of B.

Also, Rel-sets on the power set P(M) of a monoid M arise in a categorical approach to automata theory. For details of this and other applications, see [8].

A morphism f: X → Y of Rel-sets on B is an op-lax natural transformation. Thus, f consists of a function f_{b}: X_{b} → Y_{b}, for every object b, such that for every morphism β: b → b′ there is a diagram

[figure: X_{b}; X_{b′}; Y_{b}; Y_{b′}; X_{β}; –; Y_{β}; –; f_{b}; f_{b′}; ⊆]

in Rel, i.e., x →_{β} x′ ⇒ f_{b}x →_{β} f_{b′}x′.

Note that this is the notion of morphism given by Ghilardi and Meloni [4, 5] and Rosenthal [8]. A more general definition of morphism, in which the functions f_{b} are replaced by relations, is also given in [8]. Abramsky, Gay, and Nagarajan do not consider morphisms of specification structures in [1].

When B is a small category, Rel-sets and their morphisms form a locally small locally preordered 2-category Rel^{B} with f → g, if f_{b}x →_{b} g_{b}x, for all b ∈ B and x ∈ X_{b}, and consequently, x →_{β} x′ ⇒ f_{b}x →_{β} g_{b′}x′, for all β: b → b′, x ∈ X_{b}, and x′ ∈ X_{b′}. The symbol “→” is used here for a preorder to distinguish it from a partial order “≤” since both arise on the same set in §5.

3. Rel-Sets and Faithful Functors

In this section, we assume B is a small category and consider a 2-adjunction

Rel^{B} ⟵^{L} ; ⟶_{Γ} Cat/B

which gives rise to an equivalence between Rel^{B} and the category Cat_{f}/B of faithful functors over B. In particular, Γ is given by the lax fibration for the Grothendieck construction on a Rel-set.

Recall that Cat/B is the 2-slice category whose objects are functors p: E → B, morphisms are commutative triangles

[figure: E; F; B; f; p; q]

in Cat, and 2-cells are natural transformations θ: f → g such that qθ = id_{p}.

For p: E → B and an object b of B, the fiber E_{b} of E over b is the subcategory of E consisting of objects over b and morphisms over id_{b}. Let Lp denote the Rel-set with (Lp)_{b} = E_{b} and e →_{β} e′ if there exists ξ: e → e′ such that pξ = β. As is customary for slice categories, we will often suppress the explicit reference to p and write LE instead of Lp. If f: E → F is a functor over B, then f_{b}: E_{b} → F_{b} defines a morphism f: LE → LF, since e →_{β} e′ when there exists ξ: e → e′ over β: b → b′, and hence fξ: fe → fe′ over β, showing that f_{b}e →_{β} f_{b′}e′. Moreover, f → g for every 2-cell θ: f → g, since the morphism θ_{e}: fe → ge satisfy qθ_{e} = id_{pe} = id_{b}, and so f_{b}e →_{b} g_{b}e, for all e in (LE)_{b}. Thus, L: Cat/B → Rel^{B} is a 2-functor.

Note that the lax functor LE: B → Rel need not be a functor. In fact, it is unitary (i.e., identity preserving) precisely when p: E → B has discrete fibers, and it preserves composition when p satisfies the weak factorization lifting property (WFLP)

[figure: E; p; B; e; e′′; ξ′′; ·; ·; ·; ξ; e′; ·; ·; ·; ξ′; pe; pe′′; pξ′′; β; b′; β′]

i.e., for every morphism ξ′′ of E and every factorization pξ′′ = β′β in B, there exists a factorization ξ′′ = ξ′ξ in E such that pξ = β and pξ′ = β′.

This condition is a weakening of the usual Giraud-Conduché [6, 3] factorization lifting property characterizing exponentiable objects of Cat/B. In particular, it does not require the usual “zigzag” relating any two liftings of the same factorization. However, restricting to posets, p: E → B satisfies WFLP if and only if it is exponentiable in the category P os of posets and order-preserving maps [10]. The fact that WFLP arises (instead of FLP) should be clear from the discussion of exponentiability in the next section.

To define Γ: Rel^{B} → Cat/B, let X be a Rel-set on B, and consider the category E_{X} whose objects are pairs (x, b) where b is an object of B and x ∈ X_{b}, and morphisms β: (x, b) → (x′, b′) are morphisms β: b → b′ of B such that x →_{β} x′ in X. Then E_{X} is a category over B via the projection ΓX: E_{X} → B which is, in fact, a faithful functor. A morphism f: X → Y of Rel-sets gives rise to a functor Γf: E_{X} → E_{Y} over B defined by Γf(x, b) = (f_{b}x, b) and Γf(β) = β. Note that every functor g: E_{X} → E_{Y} over B is of this form, for given such a g, define f_{b}: X_{b} → Y_{b} by f_{b}(x) = π_{1}g(x, b) and f(β) = β. Then f is a morphism of Rel-sets, since

x →_{β} x′ ⇒ β: (x, b) → (x′, b′) ⇒ gβ: (f_{b}x, b) → (f_{b′}x′, b′) ⇒ f_{b}x →_{β} f_{b′}x′

and Γf = g. A 2-cell f → g induces a natural transformation θ: Γf → Γg over B given by id_{b}: (f_{b}x, b) → (g_{b}x, b) since f_{b}x →_{b} g_{b}x, for all b. Thus, Γ: Rel^{B} → Cat/B is a 2-functor whose image is the full subcategory of Cat_{f}/B of faithful functors over B.

To see that L is left adjoint to Γ, define ε: LΓ → id and η: id → ΓL, as follows. Given a Rel-set X, note that

(LΓX)_{b} = (E_{X})_{b} = {(x, b)|x ∈ X_{b}}

Then the projections (ε_{X})_{b}: (LΓX)_{b} → X_{b} define a morphism ε_{X}: LΓX → X, which is clearly a 2-natural isomorphism. Likewise, given p: E → B in Cat/B, ΓLE is the category whose objects are pairs (e, b) where e ∈ LE_{b}, i.e., pe = b, and morphisms β: (e, b) → (e′, b′) are morphisms β: b → b′ such that e →_{β} e′ in LE, i.e., there exists ξ: e → e′ in E with pξ = β. Then η_{E}: E → ΓLE, given by η_{E}(e) = (e, pe) and η_{E}(ξ) = pξ, gives rise to a 2-natural transformation η: p → Lp, such that η_{E} is full and surjective on objects, in any case, and faithful if and only if p is faithful. Moreover, the adjunction identities easily follow. Therefore, the following has been established:

3.1. Theorem. There is a 2-adjunction

Rel^{B} ⟵^{L} ; ⟶_{Γ} Cat/B

which induces an equivalence between the locally preordered 2-category Rel^{B} and the slice 2category Cat_{f}/B of faithful functors over B. As a result, Cat_{f}/B is a reflective subcategory of Cat/B with reflection ΓL.

Note that the equivalence Rel^{B} ≃ Cat_{f}/B is essentially that of Bénabou mentioned in the introduction and described by Street in [12]. But, the “op” does not appear here since the morphisms of Rel are opposite those of Mod. Also, normal (i.e., strictly identitypreserving) lax functors B^{op} → Mod are considered there in order to obtain all of Cat/B. Normality does not arise here since the identity morphisms of Rel are the diagonals. In fact, normal lax functors B → Rel correspond to faithful functors E → B whose fiber E_{b} are discrete.

Since Cat_{f}/B is a reflective subcategory of Cat/B, it is closed under limits. Using the equivalence with Rel^{B}, we get:

3.2. Corollary. Limits exist and are computed point-wise in Rel^{B}.

In the case where B a preordered set (in particular, a poset), Cat_{f}/B is the category Pr/B of preordered sets over B. Thus, Theorem 3.1 gives rise to the following equivalence which was used by Ghilardi and Meloni [4] in their relational semantics.

3.3. Corollary. If B is a preordered set, then Rel^{B} ≃ Pr/B.

4. Change of Base and Exponentiability

A functor p: E → B induces a 2-functor p^{∗}: Rel^{B} → Rel^{E}, given by (p^{∗}X)_{e} = X_{pe} with x →_{ξ} x′ whenever x →_{pξ} x′ in X, and (p^{∗}f)_{e} = f_{pe}, since f → f′ implies p^{∗}f → p^{∗}f′. A straightforward calculation shows that p^{∗} has a left adjoint Σ_{p} given by (Σ_{p}Y)_{b} = ∐_{pe=b} Y_{e} with y →_{β} y′ whenever y →_{ξ} y′ for some ξ such that pξ = β, and (Σ_{p}g)_{b} = ∐_{pe=b} g_{e}.

In this section, we will show that p^{∗} has a right adjoint if and only if p satisfies the weak factorization lifting property (WFLP) introduced in the previous section, and then establish a connection to exponentiability in Cat_{f}/B.

To begin, one easily shows that pulling back along p preserves faithful functors, i.e., if q: F → B is faithful, then so is the projection E ×_{B} F → E in the pullback diagram

[figure: E ×_{B} F; E; F; B; q; p]

and that p^{∗}: Rel^{B} → Rel^{E} corresponds (via the equivalence of Theorem 3.1) to the pullback functor Cat_{f}/B → Cat_{f}/E, also denoted by p^{∗}. Moreover, by uniqueness of adjoints, Σ_{p}: Rel^{E} → Rel^{B} corresponds to the functor obtained by first composing with p and then reflecting, i.e.,

Cat_{f}/E ⟶^{Σ_{p}} Cat/B ˆ ⟶ Cat_{f}/B

4.1. Theorem. The following are equivalent for a functor p: E → B.

(a) p^{∗}: Rel^{B} → Rel^{E} has a right 2-adjoint

(b) p^{∗}: Cat_{f}/B → Cat_{f}/E has a right 2-adjoint

(c) p satisfies the weak factorization lifting property (WFLP)

(d) The lax functor Lp: B → Rel is a non-unitary functor

Proof. Since (a)⇔(b) and (c)⇔(d) in any case, it suffices to prove (c)⇒(a) and (b)⇒(c).

For (c)⇒(a), suppose p satisfies WFLP, and define a 2-functor

Π_{p}: Rel^{E} → Rel^{B}

as follows. Given Y in Rel^{E}, let (Π_{p}Y)_{b} denote the set of functions

σ: E_{b} → ∐_{pe=b} Y_{e}

such that σe ∈ Y_{e} and σe_{1} →_{ι} σe_{2} for all ι: e_{1} → e_{2} over id_{b}, and define σ →_{β} σ′ if σe →_{ξ} σ′e′, for all ξ: e → e′ over β: b → b′.

Then (RS1*) holds, since σ →_{b} σ, for all σ ∈ (Π_{p}Y)_{b}, by definition. For (RS2*), suppose σ →_{β} σ′ and σ′ →_{β′} σ′′, where β: b → b′ and β′: b′ → b′′. To see that σ →_{β′′} σ′′ for β′′ = β′β, suppose ξ′′: e → e′′ over β′′. Applying WFLP, there exists a factorization ξ′′ = ξ′ξ such that pξ = β and pξ′ = β′. Then σe →_{ξ} σ′e′ and σ′e′ →_{ξ′} σ′′e′′, and so σe →_{ξ′′} σ′′e′′, since Y is a Rel-set over E. Therefore, σ →_{β′′} σ′′, and it follows that Π_{p}Y is a Rel-set over B.

A morphism g: Y → Z of Rel^{E} induces a function

(Π_{p}g)_{b}: (Π_{p}Y)_{b} → (Π_{p}Z)_{b}

for each b, which takes σ to the composite

E_{b} ⟶^{σ} ∐_{pe=b} Y_{e} \underrightarrow{∐ g_{e}} ∐_{pe=b} Z_{e}

A straightforward calculation shows that this is a morphism of Rel^{B}.

To see that a 2-cell g → g′ gives rise to Π_{p}g → Π_{p}g′, we must show that (Π_{p}g)_{b}σ →_{b} (Π_{p}g′)_{b}σ, for all σ ∈ (Π_{p}Y)_{b}, i.e., g_{e_{1}}σe_{1} →_{ι} g′_{e_{2}}σe_{2}, for all ι: e_{1} → e_{2} over id_{b}. Now, σe_{1} →_{ι} σe_{2} since σ ∈ (Π_{p}Y)_{b}, and so g_{e_{1}}σe_{1} →_{ι} g_{e_{2}}σe_{2} since g is a morphism. Also, g_{e_{2}}σe_{2} →_{e_{2}} g′_{e_{2}}σe_{2}, since g → g′, and so g_{e_{1}}σe_{1} →_{ι} g′_{e_{2}}σe_{2} follows from transitivity in Z.

It remains to show that p^{∗} is left adjoint to Π_{p}. For the counit ε: p^{∗}Π_{p} → id, note that (p^{∗}Π_{p}Y)_{e} = (Π_{p}Y)_{pe}, where elements are functions

σ: E_{pe} → ∐_{pe′=pe} Y_{e′}

such that σe′ ∈ Y_{e′} and σe′_{1} →_{ι′} σe′_{2} for all ι′: e′_{1} → e′_{2} over id_{pe}. Then one can show that the evaluation map (ε_{Y})_{e}: (Π_{p}Y)_{pe} → Y_{e} given by (ε_{Y})_{e}σ = σe, defines a morphism of Rel^{E}. To define the unit η: id → Π_{p}p^{∗}, note that (Π_{p}p^{∗}X)_{b} is the set of functions

σ: E_{b} → ∐_{pe=b} X_{pe}

such that σe ∈ X_{pe} and σe_{1} →_{ι} σe_{2} for all ι: e_{1} → e_{2} over id_{b}. Then the function (η_{X})_{b}: X_{b} → (Π_{p}p^{∗}X)_{b}, which takes x to the constant function at x

⌈x⌉: E_{b} → ∐_{pe=b} X_{pe}

defines a morphism of Rel^{B}. One checks that the adjunction identity holds, to complete the proof of (c)⇒(a).

For (b)⇒(c), suppose p^{∗}: Cat_{f}/B → Cat_{f}/E has a right adjoint. To see that p satisfies WFLP, suppose ξ′′: e → e′′ in E and pξ′′ = β′β, where β: pe → b′ and β′: b′ → pe′′. Then the composite β′β gives rise to a pushout in Cat_{f}/B of the form

[figure: 1; 2; 2; 3; B; β′β; β; β′]

where 2 and 3 are the categories 0 → 1 and 0 → 1 → 2, respectively.

Since p^{∗} preserves pushouts (being a left adjoint), we get a corresponding pushout in Cat_{f}/E

[figure: E ×_{B} 1; E ×_{B} 2; E ×_{B} 2; E ×_{B} 3; E; p^{∗}β′; p^{∗}β]

Since Cat_{f}/E is a reflective subcategory of Cat/E, pushouts are formed in Cat/E and reflected to Cat_{f}/E. Thus, the pushout P → E of this diagram can be constructed as follows. Let E_{β} and E_{β′} denote the subcategories of E obtained by identifying p^{∗}β and p^{∗}β′ with their images in E. Then the objects of P are the union of those of E_{β} and E_{β′}, and the morphisms are those of E_{β} and E_{β′} together with pairs (ξ, ξ′): e → e′′ such that ξ: e → e′ in E_{β} and ξ′: e′ → e′′ in E_{β′}, subject to an appropriate equivalence relation. Since ξ′′: e → e′′ corresponds to a morphism of E ×_{B} 3, and hence one of P over β′β, the desired factorization of ξ′′ follows, to complete the proof.

Recall that, for a category A with binary products, an object X is called exponentiable if the functor X × −: A → A has a right adjoint, and A is called cartesian closed if every object is exponentiable. By Corollary 3.2, Rel^{B} has products and X × Y is given by (X × Y)_{b} = X_{b} × Y_{b} with (x, y) →_{β} (x′, y′) whenever x →_{β} x′ and y →_{β} y′. It turns out that Rel^{B} is not cartesian closed, and so exponentiable objects are of interest there.

Now, it is well-known that if A is has pullbacks and p: E → B is a morphism of A, then the pullback functor p^{∗}: A/B → A/E has a left adjoint (denoted by Σ_{p}) defined by composition with p. Moreover, p^{∗} has a right adjoint (denoted Π_{p}) if and only if p: E → B is exponentiable in A/B (e.g., see [9]).

Thus, when p: E → B is faithful, it is an object of Cat_{f}/B, and so Theorem 4.1 yields:

4.2. Corollary. The following are equivalent for a faithful functor p: E → B.

(a) p^{∗}: Rel^{B} → Rel^{E} has a right 2-adjoint

(b) Lp: B → Rel is 2-exponentiable in Rel^{B}

(c) p^{∗}: Cat_{f}/B → Cat_{f}/E has a right 2-adjoint

(d) p: E → B is 2-exponentiable in Cat_{f}/B

(e) p satisfies WFLP

(f) Lp: B → Rel is a non-unitary functor

256  SUSAN NIEFIELD

Using the equivalence Cat_{f}/B ≃ Rel^{B}, one obtains: 4.3. Corollary. The following are equivalent for a Rel-set X on B.

(a) X is 2-exponentiable in Rel^{B}

(b) Given x →_{β′′} x′′ and a factorization β′′ = β′β, there exists x′ such that x →_{β} x′ and x′ →_{β′} x′′

(c) The lax functor X: B → Rel is a non-unitary functor

Also, the equivalence Rel^{B} ≃ Pr/B of Corollary 3.3 yields: 4.4. Corollary. The following are equivalent for p: E → B in Pr/B.

(a) p^{∗}: Rel^{B} → Rel^{E} has a right 2-adjoint

(b) Lp: B → Rel is 2-exponentiable in Rel^{B}

(c) p^{∗}: Pr/B → Pr/E has a right 2-adjoint

(d) p: E → B is 2-exponentiable in Pr/B

(e) p satisfies WFLP, i.e., if e ≤ e′′ in E and pe ≤ b′ ≤ pe′′ in B, there exists e′ ∈ E such that e ≤ e′ ≤ e′′ and pe′ = b′

(f) The lax functor Lp: B → Rel is a non-unitary functor

5. Application to Granularity

In [11], Stell uses unitary lax functors X: T → Rel, on a (finite) poset T, to model data varying over time. In this context, T is called a time domain and X is a dynamic set. Thus, a dynamic set is just a unitary Rel-set. The laxity is intended to account for data such as “countries or states which have had multiple episodes of existence through history, such as Austria [11].” A classification structure is then added so that objects of the data base can be further identified, for example, as roads, railways, houses, or by other features.

A classification structure is a preordered set (Φ, →) together with a partial order ≤ (denoted by ⊒ in [11]) on Φ. In practice, ϕ ≤ ϕ′ indicates that ϕ′ is a more general class than ϕ, e.g., a building is more general than a house. And, → signifies that one class can evolve into another, e.g., a child can become an adult. The structure is assumed to satisfy (C1) For all ϕ → ϕ′, there exists ψ with ϕ ≤ ψ and ϕ′ ≤ ψ.

(C2) Any set of elements in the same connected component of (Φ, ≤) has a least upper bound.

(C3) These least upper bounds preserve →, in the sense that, if some element of one such set A can evolve into an element of another set B, then lub A → lub B.

A classification of a Rel-set X is given by a family of functions λ_{t}: X_{t} → Φ, t ∈ T, such that

λ_{t}x → λ_{t′}x′, for all x → x′ x ∈ X_{t}, x′ ∈ X_{t′},

where the subscript has been omitted on x →_{β} x′ since there is at most one morphism t → t′ in T. Thus, a classification on X is just a morphism λ: X → T^{∗}Φ in Rel^{T}, where T^{∗}Φ is the image of Φ under the functor

Pr ≃ Rel^{1} ⟶^{T^{∗}} Rel^{T}

and T denotes the unique morphism T → 1. Then a classified dynamic set (in the sense of [11]) is just a unitary classified Rel-set.

Loss of detail in the time domain is represented in [11] via a simplification from T to S, which is a span

[figure: T; S; U; p; q]

of order-preserving maps, where p is injective and q is surjective. In [11], the author constructs the simplification of a classified dynamic set X over T to one over S. Properties (C1)–(C3) play a crucial role in obtaining the classification in the unitary case.

In what follows, we obtain this construction in stages. For general Rel-sets, we get a simplification from T to S via the functor

Rel^{T} ⟶^{p^{∗}} Rel^{U} ⟶^{Σ_{q}} Rel^{S}

To obtain the simplification of a dynamic set (in the sense of [11]), we first introduce a unitary reflection, and then we adapt the construction to the classified case.

Let Dyn^{T} denote the full subcategory of Rel^{T} consisting of dynamic sets, and define ¯( ): Rel^{T} → Dyn^{T} as follows. Given a Rel-set X, let ∼_{t} (or simply ∼) denote the equivalence relation on X_{t} generated by →, and let X̄_{t} = X_{t}/ ∼_{t}. For t ≤ t′, \overline{x} ∈ X̄_{t}, and \overline{x}′ ∈ X̄_{t′}, define x̄ → x̄′ if

x → x_{1} ∼_{t_{1}} x′_{1} → ⋯ → x_{n} ∼_{t_{n}} x′_{n} → x′

for some x_{1}, x′_{1}, …, x_{n}, x′_{n}. Then → is well-defined and makes X̄ into a dynamic set on T. Note that X̄ would not necessarily be unitary if T were merely a preordered set. If f: X → Y is a morphism of Rel-sets on T, then f̄_{t}: X̄_{t} → Ȳ_{t}, given by f̄_{t}(x̄) = \overline{f_{t}x}, is well-defined and provides a Rel-set morphism f̄: X̄ → Ȳ, since f is order-preserving.

5.1. Proposition. The functor ¯( ): Rel^{T} → Dyn^{T} is left 2-adjoint to the inclusion.

Proof. With the unit η_{X}: X → X̄ given by η_{X}(x) = x̄ and the counit by the “identity” functor, the adjunction identities easily follow.

Now, suppose T ⟵^{p} U ⟶^{q} S is any span of posets. Then

Dyn^{T} ⟶^{p^{∗}} Rel^{U} ⟶^{Σ_{q}} Rel^{S} ⟶^{¯( )} Dyn^{S}

gives a simplification functor for (non-classified) dynamic sets. If p is injective, then p^{∗} preserves dynamic sets, since unitary Rel-sets on T correspond to posets with discrete fibers over T, and so this simplification functor becomes

Dyn^{T} ⟶^{p^{∗}} Dyn^{U} ⟶^{Σ_{q}} Rel^{S} ⟶^{¯( )} Dyn^{S}

Next, we consider classified Rel-sets. Let Rel^{T}//Φ denote the category whose objects are classified Rel-sets on T, i.e., λ: X → T^{∗}Φ in Rel^{T}, with morphisms given by triangles

[figure: X; Y; T^{∗}Φ; f; λ; μ; ≤]

i.e., morphisms f: X → Y in Rel^{T} such that λ_{t}x ≤ μ_{t}f_{t}x, for all x ∈ X_{t}.

Given a morphism p: U → T of posets, it is easy to show that the adjunction Σ_{p} ⊣ p^{∗} restricts to

Rel^{U}//Φ ⟶^{Σ_{p}} ; ⟵_{p^{∗}} Rel^{T}//Φ

Thus, for a span T ⟵^{p} U ⟶^{q} S, we get a simplification functor for classified Rel-sets

Rel^{T}//Φ ⟶^{p^{∗}} Rel^{U}//Φ ⟶^{Σ_{q}} Rel^{S}//Φ

Note that (C1)–(C3) were not needed for this general (not necessarily unitary) case which was not considered in [11].

Now, let Dyn^{T}//Φ be the full subcategory of Rel^{T}//Φ consisting of classified dynamic sets. Then the reflection ¯( ): Rel^{T} → Dyn^{T} extends to the classified case, as follows. Given a classified Rel-set λ: X → T^{∗}Φ, using (C1) and (C2), define λ̄_{t}: X̄_{t} → Φ by λ̄_{t}x̄ = lub{λ_{t}a|a ∼ x}. Then, by property (C3), λ̄ is a classification on X̄, i.e.,

x̄ → x̄′ ⇒ λ̄_{t}x̄ → λ̄_{t′}x̄′

for all x ∈ X_{t}, x′ ∈ X_{t′}, and t ≤ t′. To see that ¯( ): Rel^{T}//Φ → Dyn^{T}//Φ is a functor, suppose f: X → Y is a morphism of classified Rel-sets. Then so is f̄, that is,

[figure: X̄; Ȳ; T^{∗}Φ; f̄; λ̄; μ̄; ≤]

since λ̄_{t}x̄ = lub{λ_{t}a|a ∼ x} ≤ lub{μ_{t}f_{t}a|a ∼ x} ≤ lub{μ_{t}f_{t}a|f_{t}a ∼ f_{t}x} ≤ lub{μ_{t}b|b ∼ f_{t}x} = μ̄_{t}f̄_{t}x̄.

5.2. Lemma. The functor ¯( ): Rel^{T}//Φ → Dyn^{T}//Φ is left adjoint to the inclusion.

Proof. It suffices to show that the unit η_{X}: X → X̄ (given by η_{X}(x) = x̄ in the proof of Proposition 5.1) is a morphism of Dyn^{T}//Φ. But, this is clear, since λ_{t}x ≤ lub{λ_{t}a|a ∼ x} = λ̄_{t}x̄ = λ̄_{t}η_{t}x.

Thus, we get:

5.3. Theorem. The simplification of classified dynamic sets relative to the span T ⟵^{p} U ⟶^{q} S (in the sense of [11]) is given by

Dyn^{T}//Φ ⟶^{p^{∗}} Rel^{U}//Φ ⟶^{Σ_{q}} Rel^{S}//Φ ⟶^{¯( )} Dyn^{S}//Φ

We conclude with a consideration of right adjoints to the simplification functors.

5.4. Theorem. If T ⟵^{p} U ⟶^{q} S is a span of preordered sets, then the simplification functor Rel^{T} ⟶^{p^{∗}} Rel^{U} ⟶^{Σ_{q}} Rel^{S} has a right adjoint if and only if p^{∗} does, i.e., p is a WFLP map.

Proof. Consider the corresponding composite Pr/T ⟶^{p^{∗}} Pr/U ⟶^{Σ_{q}} Pr/S. By [9, Proposition 1.1], a functor F: Pr/T → Pr/S has a right adjoint if and only if

Pr/T ⟶^{F} Pr/S ⟶^{Σ_{S}} Pr

does, and so the desired result follows.

5.5. Theorem. If T ⟵^{p} U ⟶^{q} S is a span of posets and p is an injective WFLP map, then the simplification functor

Dyn^{T} ⟶^{p^{∗}} Dyn^{U} ⟶^{Σ_{q}} Rel^{S} ⟶^{¯( )} Dyn^{S}

has a right 2-adjoint.

Proof. Since Σ_{q}: Rel^{U} → Rel^{S} and ¯( ): Rel^{S} → Dyn^{S} have right adjoints and q^{∗} preserves dynamic sets, it suffices to show that p^{∗} has a right adjoint. Now, p^{∗}: Rel^{T} → Rel^{U} does by Corollary 4.4, since p satisfies WFLP, and one can show using the description in the proof of Theorem 4.1, that Π_{p} preserves dynamic sets, since p is injective, and the desired result follows.

For the classified case, the situation is more complicated. In particular, Π_{p} cannot be easily adapted unless we impose conditions on Φ which may not make sense for the intended interpretation [11] of the relations on Φ. For example, taking T = {0, 1} and p to be the inclusion of U = {1}, one can show that Φ would need an element ϕ_{0} such that ϕ ≤ ϕ_{0} and ϕ_{0} → ϕ, for all ϕ ∈ Φ, i.e., a class that is more general than and could evolve into any other class. This can be seen using Y = T^{∗}Φ and the description of Π_{p}Y in Theorem 4.1. On the other hand, using the inclusion of U = {0} in T, one can show that Φ would need an element ϕ_{1} such that ϕ ≤ ϕ_{1} and ϕ → ϕ_{1}, for all ϕ ∈ Φ, i.e., ϕ_{1} would be a class that is more general than any other class and such that any class could evolve into ϕ_{1}.

References

[1] S. Abramsky, S. Gay, and R. Nagarajan, Specification structures and propositionsas-types for concurrency, Logics for Concurrency - Structure versus Automata (8th Banff Higher Order Workshop, August 27 - September 3, 1995, Proceedings), Springer Lecture Notes in Computer Science 1043 (1996) 5–40.

[2] Bénabou, Introduction to bicategories, Reports of the Midwest Category Theory Seminar, Springer Lecture Notes in Math. 47 (1967) 1–77

[3] F. Conduché, Au sujet de l’existence d’adjoints à droite aux foncteurs “image réciproque” dans la catégorie des catégories, C. R. Acad. Sci. Paris 275 (1972) A891–894.

[4] S. Ghilardi and G. Meloni, Relational and topological semantics for temporal and modal predicative logic, Atti del congresso ‘Nuovi problemi della logica e della scienza’ Viareggio, Gennaio 1990 vol. II – Logica, CLUEB Bologna (1991) 59–77.

[5] S. Ghilardi and G. Meloni, Relational and partial variable sets and basic predicate logic, J. Symbolic Logic 61 (1996) 843–872.

[6] J. Giraud, Méthode de la déscente, Bull. Math. Soc. France, Memoire 2 (1964).

[7] G. M. Kelly and R. Street, Review of the elements of 2-categories, Category Seminar, Sydney 1972/73, Springer Lecture Notes in Math. 420 (1974) 75–103.

[8] K. R. Rosenthal, The Theory of Quantaloids, Addison Wesley Longman, 1996.

[9] S. B. Niefield, Cartesianness topological spaces, uniform spaces, and affine schemes, J. Pure Appl. Alg. 23 (1982) 147–167.

[10] S. B. Niefield, Exponentiable morphisms: posets, spaces, locales, and Grothendieck toposes, Theory and Applications of Categories 8 (2001) 16–32.

[11] J. G. Stell, Granularity in change over time, in: Duckham, M., Goodchild, M., and Worboys, M. Foundations of Geographic Information Science, Taylor and Francis (2003) 95–115.

[12] R. Street, Powerful functors, expository note, September 2001.

Union College, Department of Mathematics Schenectady, NY 12308, USA

Email: niefiels@union.edu

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/12/7/12-07.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@barrs.org, Associate Managing Editor Lawrence Breen, Université Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of Wales Bangor: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Palo Alto Research Center: paiva@parc.xerox.com Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca