[000T] -- Synthetic topos theory

[000T] Lemma

Let $U$ be a universe. Then étale morphisms in $\mathord {\textnormal {\textsf {Topos}}}(U)$ has the left cancellation property. That is, for morphisms $f:Y\rightarrow X$ and $g:Z\rightarrow Y$ in $\mathord {\textnormal {\textsf {Topos}}}(U)$ , if $f$ and $f\circ g$ are étale, then so is $g$ .

Proof

Let $X$ be a $U$ -topos, let $a,b:\mathord {\textnormal {\textsf {Sh}}}(X)$ be objects, and let $F:\mathord {\textnormal {\textsf {Sh}}}(X)/a\rightarrow \mathord {\textnormal {\textsf {Sh}}}(X)/b$ be a morphism in $\mathord {\textnormal {\textsf {Logos}}}(U)\backslash \mathord {\textnormal {\textsf {Sh}}}(X)$ . By [000I], $F$ is equivalent to the pullback functor ${u}^{*}$ for some morphism $u:b\rightarrow a$ . Let $s:\mathord {\textnormal {\textsf {Sh}}}(X)/a$ be the object represented by $u$ . We have the equivalence $\mathord {\textnormal {\textsf {Sh}}}(X)/b\simeq (\mathord {\textnormal {\textsf {Sh}}}(X)/a)/s$ . Then [000P] applies.