Joyal's CatLab Trivial fibrations in a topos

Proof

We shall prove that the conditions of the proposition here are satisfied. We have $\mathcal{R} =\mathcal{L}^\pitchfork$ by definition of $\mathcal{R}$. Hence the class $\mathcal{R}$ is closed under (domain) retracts by the proposition hereThe class $\mathcal{L}$ is obviously closed under (codomain) retracts. It remains to show that every map $f:A\to B$ in $\mathbf{E}$ admits a factorisation $f=p u:A\to E\to B$ with $u\in \mathcal{L}$ and $p\in \mathcal{R}$. We shall first prove that every object can be embedded into an injective object. Let us first show that the Lawvere object $\Omega\in \mathbf{E}$ is injective. For this we have to show that the map

induced by $u$ is surjective for every monomorphism $u$. For every object $A\in \mathbf{E}$, let us denote the set of subobjects of $A$ by $P(A)$. A map $u:A\to B$ in $\mathbf{E}$ induced a map $u^*:P(B)\to P(A)$ which associates to a subobject $S\to B$ its inverse image $u^*(S)\to A$. This defines a contravariant functor $P:\mathbf{E}^o\to \mathbf{Set}$ which is represented by $\Omega$ (with universal subobject $t:1\to \Omega$). Hence the map $hom(u,\Omega)$ is isomorphic to the map $u^*:P(B)\to P(A)$. But the map $u^*$ is surjective when $u$ is monic, since we have $u^*u(S)=S$ for every subobject $S\to A$ in this case. We have proved that the object $\Omega$ is injective. Let us now show that every object can be embedded into an injective object. It is easy to verify that if $Z$ is an injective object, then so is the object $Z^A$ for any object $A$. In particular, the object $\Omega^A$ is injective for any object $A$. But the singleton map $A\to \Omega^A$ (which “classifies” the diagonal $A\to A\times A$) is monic by a classical result. This show that $A$ can be embedded into an injective object. We can now show that every map $f:A\to B$ in $\mathbf{E}$ admits a factorisation $f=pu:A\to E\to B$ with $u\in \mathcal{L}$ and $p\in \mathcal{R}$. But a map $p:Z\to B$ is a trivial fibration iff the object $(Z,p)$ of the topos $\mathbf{E}/B$ is injective. Hence the factorisation can be obtained by embedding the object $(A,f)$ of the topos $\mathbf{E}/B$ into an injective object of this topos. The existence of the factorisation is proved.