nLab simulation

Simulations

Simulations

Idea

A simulation is a morphism of coalgebras for an endofunctor.

Definition

Let CC be a category, and let F:CCF\colon C \to C be an endofunctor. Recall that a coalgebra of FF is an object XX of CC equipped with a morphism θ:XF(X)\theta\colon X \to F(X).

Definition

Given two coalgebras X,XX, X' of FF, a simulation of XX in XX' is a morphism s:XXs\colon X \to X' in CC such that F(s)θ=θsF(s) \circ \theta = \theta' \circ s. That is, this diagram commutes:

X θ F(X) s F(s) X θ F(X) \array { X & \overset{\theta}\to & F(X) \\ \llap{s}\downarrow & & \downarrow\rlap{F(s)} \\ X' & \underset{\theta'}\to & F(X') }

The terminology comes from computer science, and we should probably explain what it’s about.

Examples

Relations

Consider the category of sets and the (covariant) power set functor 𝒫\mathcal{P}. A coalgebra of 𝒫\mathcal{P} is a set XX equipped with a function θ:X𝒫(X)\theta\colon X \to \mathcal{P}(X), which is the same thing as a binary relation \prec on XX. To fix the notation, we write aba \prec b (aa precedes bb) if aθ(b)a \in \theta(b).

Then in concrete terms, a simulation of XX in XX' is a function s:XXs\colon X \to X' such that

  • s(a)s(b)s(a) \prec' s(b) whenever aba \prec b, and
  • t=s(a)t = s(a) for some aba \prec b whenever ts(b)t \prec' s(b).

Simulations are commonly used as morphisms between sets equipped with well-founded or extensional relations. In particular, between well-ordered sets (sets equipped with relations that are both well-founded and extensional, as well as transitive), a simulation (if it exists) is unique, and we recover the usual ordered class of ordinal numbers as a thin category.

Open maps in algebraic set theory

In their book Algebraic Set Theory, Joyal and Moerdijk present the notion of a pretopos equipped with a class of open maps. As they remark, every presheaf category carries a canonical class of open maps. We reformulate their notion of canonical open map for an example of primary interest to them, the category of forests, in coalgebraic terms.

The category of forests? is by definition the category of presheaves over the first infinite ordinal ω\omega. Concretely, a forest FF is a diagram of sets and functions

F n+1F nF 1F 0.\ldots \to F_{n+1} \to F_n \to \ldots \to F_1 \to F_0.

If yF n+1y \in F_{n+1} maps to xF nx \in F_n, we call yy a predecessor of xx.

The successor map s:ωωs: \omega \to \omega induces a pullback functor

s *=Set s op:Set ω opSet ω op.s^\ast = Set^{s^{op}}: Set^{\omega^{op}} \to Set^{\omega^{op}}.

Let PP be the covariant power-object functor on the presheaf topos. Each forest FF carries a canonical coalgebra structure over the endofunctor Ps *P s^\ast. Namely, the structure is a presheaf map θ FPs *F\theta_F \to P s^\ast F that corresponds to the subobject

RF×s *FR \hookrightarrow F \times s^\ast F

where the subset R nR_n is the set of pairs (x,y)F n×F n+1(x, y) \in F_n \times F_{n+1} such that yy is an immediate predecessor of xx.

If ϕ:FG\phi: F \to G is a map of forests, in other words if the functions ϕ n:F nG n\phi_n: F_n \to G_n collectively preserve the predecessor relation, then we have an inclusion

F ϕ G θ F θ G Ps *F Ps *ϕ Ps *G\array{ F & \stackrel{\phi}{\to} & G \\ ^\mathllap{\theta_F} \downarrow & \leq & \downarrow^\mathrlap{\theta_G} \\ P s^\ast F & \underset{P s^\ast \phi}{\to} & P s^\ast G }

where \leq comes from the internal poset structure of Ps *GP s^\ast G. If this inclusion is an equality; in other words, if ϕ\phi is a coalgebra map or simulation over Ps *P s^\ast, then we also say (following Joyal and Moerdijk) that ϕ\phi is open. Alternatively, we could say that ϕ\phi is open if the maps ϕ n\phi_n collectively preserve and reflect the predecessor relation.

Pursuing this more concretely: the composite θ Gϕ\theta_G \circ \phi corresponds to the subobject SS of F×s *GF \times s^\ast G occurring in the pullback

S R G F×s *G ϕ×1 G×s *G\array{ S & \to & R_G \\ \downarrow & & \downarrow \\ F \times s^\ast G & \underset{\phi \times 1}{\to} & G \times s^\ast G }

so that S nF n×G n+1S_n \subseteq F_n \times G_{n+1} consists of pairs (x,y)(x, y) such that yy is a predecessor of ϕ n(x)\phi_n(x) in GG. The composite Ps *(ϕ)θ FP s^\ast(\phi) \circ \theta_F corresponds to the subobject SS' of F×s *GF \times s^\ast G occurring in an image factorization

R F S F×s *F 1×s *ϕ F×s *G\array{ R_F & \twoheadrightarrow & S' \\ \downarrow & & \downarrow \\ F \times s^\ast F & \underset{1 \times s^\ast \phi}{\to} & F \times s^\ast G }

so that (taking advantage of the fact that image factorizations in a presheaf topos are computed objectwise) S nF n×G n+1S_{n}' \subseteq F_n \times G_{n+1} consists of pairs (x,y)(x', y') such that y=ϕ n+1yy' = \phi_{n+1} y for some predecessor yy of xx in FF. The equality of subobjects S=SS = S' matches the notion of open map given in Algebraic Set Theory.

Remark: Joyal and Moerdijk actually refine this idea as follows. Instead of taking forests to be set-valued presheaves, they take them to be presheaves over ω\omega valued in a given pretopos CC equipped with a class of small maps (which are defined axiomatically). Then, a small forest is a diagram in CC of the form

F n+1F nF 1F 0\ldots \to F_{n+1} \to F_n \to \ldots \to F_1 \to F_0

where each map F n+1F nF_{n+1} \to F_n and F 01F_0 \to 1 is small. On the other hand, the small map axioms guarantee that small subobjects are representable by a functor P small:CCP_{small}: C \to C. This induces a functor P small:C ω opC ω opP_{small}: C^{\omega^{op}} \to C^{\omega^{op}} on the category of forests, and analogous to what we described above, a small forest can be construed in terms of a coalgebra structure FP small(s *F)F \to P_{small} (s^\ast F).

Last revised on January 29, 2016 at 15:12:46. See the history of this page for a list of all contributions to it.