Seeing that the subobject fibration is a fibration

69 Views Asked by At

Let $\mathcal{B}$ be a category with pullbacks. We have that $cod:\mathcal{B}^\rightarrow\to\mathcal{B}$ is a fibration, with the Cartesian arrow over $k:X\to cod(g:Y\to Z)$ given by the pullback square

If $g$ is a monomorphism then so is $g_k$, so the above commutative square is an arrow between monomorphisms in $\mathcal{B}^\rightarrow$ which maps to $k$ under $cod$ and consequently the restriction of $cod$ to the subcategory ${\sf Mono}(\mathcal{B})\subset\mathcal{B}^\rightarrow$ consisting of monomorphisms is still a fibration.

To pass to the subcategory ${\sf Sub}(\mathcal{B})$ of subobjects in $\mathcal{B}$ we need to take a skeleton of ${\sf Mono}(\mathcal{B})$, and this is where I have difficulty seeing that $cod$ is still a fibration restricted to this skeleton. In particular we no longer have that $g_k$ is an arrow in the skeleton ${\sf Sub}(\mathcal{B})$ even if $g$ is, only that $g_k\cong p$ for some monomorphism $p:A\rightarrowtail B$ in ${\sf Sub}(\mathcal{B})$. We then have that $(A,g_k\circ \cong_0,k_g\circ\cong_0)$ is still a pullback of $k$ and $g$ and $(k_g\circ\cong_0,k\circ\cong_1)$ is an arrow in ${\sf Sub}(\mathcal{B})$ from $p$ to $g$, but it isn't above $k$ under $cod$ anymore, it's above $k\circ\cong_1$ as illustrated below

and so doesn't satisfy us as a Cartesian arrow over $k$. We can try to rearrange the square so it's over $k$ again as below

but then it isn't obvious to me that $\cong_1\circ p=g_k\circ\cong_0$ is in ${\sf Sub}(\mathcal{B})$ despite being a mono, only that it's isomorphic to a mono in our skeleton once again. How do we remedy this?

If $\cong_1\circ p$ is in our skeleton then we're good to go, but it seems to me that it isn't necessarily. The only solution I see in this case is to take ${\sf Sub}(\mathcal{B})$ to be a specific skeleton comprised of pullbacks, but this isn't mentioned anywhere specifically in the text I'm working through (Categorical Logic and Type Theory by Jacobs) or on the web that I can find, and seems like a clunky solution. Any assistance is appreciated.