Dear Joe, This is the "polynomial category" construction described in Lambek's and Scott's "Introduction to Higher Categorical Logic" section I.5. (I don't think they describe it as a pushout, though that is very natural and must be well known. For instance, this came up in a google search for ' "polynomial category" pushout': Pavlovic, D. Geometry of abstraction in quantum computation <https://arxiv.org/pdf/1006.1010.pdf>, p. 9). Best, Joj On Thu, Nov 14, 2019 at 6:57 AM Joseph Collins <joseph.collins@strath.ac.uk> wrote:
Hey all
Suppose that we have a category A. If we want to formally add a single morphism, say f:X -> Y, where X,Y are in A, but f is not in A, we can do the following: we look at the discrete category containing only X and Y - let us denote that as (X Y) - and the category with two objects and only a single morphism between them. Let's call this one (X -> Y).
There are natural embeddings (X Y) -> A and (X Y) -> (X -> Y). We take the pushout of these functors, and as one might expect, we get the union of A and (X -> Y). This is basically A, but with an extra morphism formally added in. Let's call this new morphism f and the new category A_f. This category is not particularly interesting, but I can then quotient it by some equations involving f and it becomes more interesting.
I don't think that I am doing anything particularly modern, and I expect that someone else will have done something similar in the past, but my search has not been very fruitful. Does anyone have any references that they can throw my way?
Thanks Joe
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]