Saturday, 12 June 2010

ct.category theory - Pushout over a whole diagram

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:crightarrowe 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:crightarrowe '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