Given two coalgebras of , a simulation of in is a morphism in such that . That is, this diagram commutes:
The terminology comes from computer science, and we should probably explain what it’s about.
Consider the category of sets and the (covariant) power set functor . A coalgebra of is a set equipped with a function , which is the same thing as a binary relation on . To fix the notation, we write ( precedes ) if .
Then in concrete terms, a simulation of in is a function such that
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.
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.
If maps to , we call a predecessor of .
The successor map induces a pullback functor
Let be the covariant power-object functor on the presheaf topos. Each forest carries a canonical coalgebra structure over the endofunctor . Namely, the structure is a presheaf map that corresponds to the subobject
where the subset is the set of pairs such that is an immediate predecessor of .
If is a map of forests, in other words if the functions collectively preserve the predecessor relation, then we have an inclusion
where comes from the internal poset structure of . If this inclusion is an equality; in other words, if is a coalgebra map or simulation over , then we also say (following Joyal and Moerdijk) that is open. Alternatively, we could say that is open if the maps collectively preserve and reflect the predecessor relation.
Pursuing this more concretely: the composite corresponds to the subobject of occurring in the pullback
so that consists of pairs such that is a predecessor of in . The composite corresponds to the subobject of occurring in an image factorization
so that (taking advantage of the fact that image factorizations in a presheaf topos are computed objectwise) consists of pairs such that for some predecessor of in . The equality of subobjects 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 valued in a given pretopos equipped with a class of small maps (which are defined axiomatically). Then, a small forest is a diagram in of the form
where each map and is small. On the other hand, the small map axioms guarantee that small subobjects are representable by a functor . This induces a functor on the category of forests, and analogous to what we described above, a small forest can be construed in terms of a coalgebra structure .