Suppose I have a diagram $D$ over a category $C$, where $D$ (as a graph) is a single-rooted directed acyclic graph, and all 'joins' in this DAG are actually colimits. Let the root of this diagram be the object $c$ of $C$. Suppose I also have a (new) arrow $a : crightarrow e$ where $e$ is not in diagram $D$. From this arrow, one can successively compute a number of pushouts, to obtain a new diagram $D'$ "over" $D$. [Assume that by base category $C$ has all filtered colimits, so that this all makes sense].
Question: what is the proper name for this construction? Where can I find a solid mathematical presentation of this? [I have seen this used in a number of places, but never given a proper reference]
Motivation: My category $C$ is a category of (presentations of) theories (with sorts, signatures and axioms), and my diagram $D$ is built by successively extending a base theory $c$ by adding new sorts/signatures/axioms and explicit pushouts. If I now extend the base theory $c$ in a 'new' direction, I should be able to 'replay' the extension given by arrow $a:crightarrow e$ 'over' all of $D$ to get a (parallel) diagram of theories $D'$ based on $e$. The aim is to maximize re-use of concepts (given by each extension).
[I realize that such a construction might well give me inconsistent theories, i.e. that some of the nodes in $D$ and $D'$ will have no models. They will, however, be perfectly fine as (presentations of) inconsistent theories.]
No comments:
Post a Comment