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.