name this "hybrid" categorical construction

Question

I've found a general categorical construction which I'm not familiar with.

Suppose that we have the square shown, with categories $A$, $B_i$, $C$ and functors $F_i$ and $G_i$ such that the diagram commutes ($G_0 F_0 = G_1 F_1$), and that $A$ is discrete in the sense that it has only the identity morphisms.

$$ \begin{array}{rcccl} A & {} & \xrightarrow{F_0} & {} & B_0 \\ {} & {} & {} & {} & {} \\ {\scriptstyle F_1}\downarrow & {} & {} & {} & \downarrow{\scriptstyle G_0} \\ {} & {} & {} & {} & {} \\ B_1 & {} & \xrightarrow{G_1} & {} & C \\ \end{array} $$

Then define $A^*$ as follows: the objects of $A^*$ are the same as the objects of $A$; a morphism $m \in A^*(X, Y)$ is a pair $(m_0, m_1)$ such that $m_i \in B_i(F_i(X), F_i(Y))$ and $G_0(m_0) = G_1(m_1)$. I believe that this makes $A^*$ a category with obvious functors $A \to A^*$, $A^* \to B_i$ making the whole diagram commute.

$$ \begin{array}{rcccl} A & {} & \xrightarrow{F_0} & {} & B_0 \\ {} & \searrow & {} & \nearrow & {} \\ {\scriptstyle F_1}\downarrow & {} & A^* & {} & \downarrow{\scriptstyle G_0} \\ {} & \swarrow & {} & {} & {} \\ B_1 & {} & \xrightarrow{G_1} & {} & C \\ \end{array} $$

For example, suppose $A$ is the discrete category $\operatorname{Top}_{\operatorname{dis}}$ of topological spaces with identity morphisms, $B_0$ is the usual category $\operatorname{Top}$, $B_1$ is the category $\operatorname{Set}_{\operatorname{inj}}$ of sets with injective maps between them, and $C$ is the usual category $\operatorname{Set}$. The functors are all the obvious inclusions/forgettings. Then $A^*$ is the category of topological spaces with injective continuous maps between them. It's a kind of hybrid between $\operatorname{Top}$ and $\operatorname{Set}_{\operatorname{inj}}$.

$$ \begin{array}{rcccl} \operatorname{Top}_{\operatorname{dis}} & {} & \xrightarrow{} & {} & \operatorname{Top} \\ {} & \searrow & {} & \nearrow & {} \\ {}\downarrow & {} & A^* & {} & \downarrow{} \\ {} & \swarrow & {} & {} & {} \\ \operatorname{Set}_{\operatorname{inj}} & {} & \xrightarrow{} & {} & \operatorname{Set} \\ \end{array} $$

Questions

• Does this all work?
• Is this a known construction? In particular, does it have some nice universal property?

Answer 1

$A^*$ is the functor pullback (thank you to responders above) combined with the "inverse image of a functor" described in my other question here. We can get the pullback $P$, then its universal property gives us a functor $F: A \to P$ with a commutative diagram. Then in the notation of that other question, we can factor $F$ into $A \to F^{-1}(P) \to P$, and take $A^* = F^{-1}(P)$.

I'm still not sure whether this is useful. I need to think some more about the principle of equivalence invariance which responders have mentioned.

Answer 2

Here is a better construction, namely the pullback, which makes no mention of $A$ (which is doing no work in your example): the objects are pairs $(c_0, c_1)$ where $c_i \in \text{Ob}(B_i)$ such that $G_0(c_0) = G_1(c_1)$. The morphisms $(c_0, c_1) \to (d_0, d_1)$ are pairs $(f_0, f_1)$ where $f_i \in \text{Hom}(c_i, d_i)$ such that $G_0(f_0) = G_1(f_1)$ (note that to state this condition we need the corresponding condition on objects first).

In your example, once you've picked a topological space $c_0$ then $c_1$ is constrained to be the underlying set of $c_0$ which is why you didn't see the interesting behavior on objects. But in general this construction behaves interestingly on objects as well.

However, it has one substantial drawback: it is not invariant under equivalence of (diagrams of) categories. That is, it really depends on (diagrams of) categories up to isomorphism rather than equivalence, which is generally a bad sign in category theory. There is a better-behaved construction which replaces the equality $G_0(c_0) = G_1(c_1)$ with an isomorphism called the homotopy pullback. There is also a lax version which replaces the equality with a morphism, not necessarily an isomorphism, which I guess should be called the lax 2-pullback or something but which is more conventionally called the comma category.