[000U] -- Synthetic topos theory

[000U] Proposition

Let $$U$$ be a universe. Then étale morphisms in $\mathord {\textnormal {\textsf {Topos}}}(U)$ are closed under diagonal. That is, if a morphism $f:Y\rightarrow X$ in $\mathord {\textnormal {\textsf {Topos}}}(U)$ is étale, then so is the diagonal morphism $Y\rightarrow Y\mathbin {{}_{f}\mathord {\times _{f}}}Y$ .

Proof

The diagonal morphism in question is a section of the first (or second) projection $Y\mathbin {{}_{f}\mathord {\times _{f}}}Y\rightarrow Y$ . By [000T] and [000Q], it suffices to show that the first projection is étale, but this follows from [000S].