Fibrations and opfibrations

Motivation: To understand the full power of the quotient-kernel adjunction $$\leftcat\graphsoverx \mathrel{\leftadj{\mathop\longrightarrow\limits^Q} \atop \rightadj{\mathop\longleftarrow\limits_K}} \rightcat\setsunderx$$ we need to understand precisely the relation between
the category $\setsunderx$ and the base category $\Set$.
The aspect of that relation that is most useful in this context
is summarized by the statement that
$\setsunderx$ is a discrete opfibration over $\Set$ that reflects isomorphisms.
It is the purpose of this document to explain
exactly what that means and why it is true in this situration.

First, let us recall the definition of the category $\setsunderx$ of sets under $X$,
where $X$ is a given, fixed, set in $\Set$.
An arrow of $\setsunderx$ is a commutative triangle in $\Set$ of the form \[\begin{array}{c} && X &&\\ & \llap{\raise4pt\hbox{$f$}} \swarrow && \searrow\rlap{\raise4pt\hbox{$g$}} &&&.\\ Y && \xrightarrow[\textstyle h]{} && Z \end{array}\] Here $X \xrightarrow f Y$ and $X \xrightarrow g Z$ (arrows in $\Set$) are objects of $\setsunderx$.
So when the arrow $Y \xrightarrow h Z$ in $\Set$ satisfies the condition $fh=g$ in $\Set$,
then it is not only an arrow $Y \xrightarrow h Z$ in $\Set$,
but also an arrow $f \xrightarrow h g$ in $\setsunderx$.
Thus we have \[\begin{align} \hom f {(\setsunderx)} g & \buildrel \text{def} \over \equiv \{\,\text{arrows in } \setsunderx \text{ from $f$ to $g$}\,\}\\ &\buildrel \text{def} \over \equiv \{\,Y\xrightarrow h Z\text{ in $\Set$} \mid \text{$h$ extends $g$ over $f$}\,\} \subseteq \hom Y \Set Z . \end{align}\]

So we have a (canonical) projection functor \[\begin{array}{c} \setsunderx & \xrightarrow{\textstyle P} & \Set\\ X \xrightarrow f Y & \mapsto & Y\\ f\xrightarrow h g & \mapsto & h \end{array}\] which is faithful $\big( \hom f {(\setsunderx)} g \xrightarrow{\textstyle \hom f P g} \hom {fP=Y} \Set {gP=Z}$ is injective$\big)$.
It is useful to depict this functor vertically: \[\begin{array}{} \setsunderx & : & X \xrightarrow f Y & , & f \xrightarrow h g\\ \llap P\big\downarrow & : & \mapsdownto && \mapsdownto \\ \Set & : & Y & , & Y \xrightarrow h Z \end{array}\] Thus we speak of the objects of the “fiber of $P$ over $Y$” as being
all the functions from $X$ to $Y$ in $\Set$, i.e., $\hom X \Set Y$.
Further, given a function $Y \xrightarrow h Z$,
we have the function “post-composition under $X$”, $\hom X \Set Y \xrightarrow{\hom X \Set h} \hom X \Set Z\,$,
taking the objects of $P^{-1}(Y)$, the fiber over $Y$
to the objects of $P^{-1}(Z)$, the fiber over $Z$.

We have defined the fibers of the functor $P$;
what property makes it a discrete opfibration? It is this:
Given the situation \[\begin{array}{} \setsunderx & : & f\\ \llap P\big\downarrow\\ \Set & : & Y & \xrightarrow[h]{} & Z \end{array}\] with $Y \xrightarrow h Z$ an arrow in the base category $\Set$
and $f$ an object in the fiber over $Y$,
there exists a unique pair of
a $g$ in the fiber over $Z$ and
an arrow $f\to g$ in the over-category $\setsunderx$ which is over $h$ (taken to $h$ by $P$),
namely the solution \[\begin{array}{} \setsunderx & : & f & \xrightarrow h & fh \\ \llap P\big\downarrow\\ \Set & : & Y & \xrightarrow[h]{} & Z \end{array}\] By the way, the arrow $h$ in the over-category in this situation
is an example of what is called an “opcartesian arrow.”

---

An aside:
To express the discrete opfibration condition in terms of internal category theory,
we have the following pullback in the category of very large sets.
(The vertices of this diagram are large categories,
thus objects not in the category of large categories,
but rather in a yet larger category.
The diagram uses the usual notation for internal categories:
$()_0$ for the object of objects, $()_1$ for the object of arrows,
and $()_1 \mathrel{\mathop\rightrightarrows\limits^{d_0}_{d_1}} ()_0$ for the source and target arrows.) \[\begin{array}{} \exists!(f \xrightarrow h fh) & \in & (\setsunderx)_1 & \xrightarrow{P_1} & \Set_1 & \ni & \forall h\\ &&\llap{d_0}\big\downarrow & & \big\downarrow \rlap{d_0}\\ \forall f & \in & (\setsunderx)_0 & \xrightarrow[P_0]{} & \Set_0 & \ni & \forall Y \end{array}\] In words, for all compatible choices of $f$, $h$, and $Y$,
there exists a unique arrow, as shown, in $\setsunderx$ which maps to $f$ and $h$.

---

We also have that $P$ reflects isomorphisms.
What that means is:
If $f \xrightarrow h g$ is an arrow in the overcategory $\setsunderx$, and
$hP$ has an inverse in the base category,
then $h$ has an inverse in the overcategory as well.

There really is something to be proved here.
We must show:
If we have a diagram in $\Set$ \[\begin{array}{} X &\xrightarrow f & Y\\ \Vert && \llap h \downarrow\uparrow\rlap k\\ X & \xrightarrow[g]{} & Z \end{array}\] with $fh=g$, and $h$ has an inverse, say $k$, in $\Set$,
then $h$ also has an inverse in $\setsunderx$.
We show this by showing that $k$, under those circumstances, is an arrow in $\setsunderx$,
which is then an inverse to $h$ there as well as in $\Set$.
To show $k$ is an arrow in $\setsunderx$
we first note that h invertible in $\Set$ implies $h$ is monic there.
Then the equalities $$gkh \xlongequal{k=h^{-1}} g 1_Z = g \xlongequal{f \xrightarrow h g} fh$$ imply $gk=f$, so $k$ is indeed an arrow in $\setsunderx$.