Let \(T\) be a base type theory. We work in \(T\). Let \(X_{1}\) and \(X_{2}\) be toposes. We say a morphism \(f:X_{1}\rightarrow X_{2}\) is essential if \({f}^{*}:\mathcal {S}(X_{2},0)\rightarrow \mathcal {S}(X_{1},0)\) has a left adjoint \({f}_{!}\).
[003O] Essential morphisms
Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. We say a point \(a\) of \(X\) is essential if the morphism \(\_\mapsto a:\mathord {\textnormal {\textsf {1}}}\rightarrow X\) is essential.
Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos and let \(a\) be an essential point of \(X\). By definition, the inverse image functor \({a}^{*}:\mathcal {S}(X,0)\rightarrow \mathcal {U}(0)\) has the left adjoint \({a}_{!}\) and thus corepresentable by \({a}_{!}(\mathord {\textnormal {\textsf {1}}})\). We refer to \({a}_{!}(\mathord {\textnormal {\textsf {1}}})\) as \(\mathord {\textnormal {\textsf {e}}}_{a}\).
For an essential point \(a:X\) of a topos \(X\), the hom functor \(A\mapsto \mathord {\textnormal {\textsf {Hom}}}_{\mathcal {S}(X,0)}(\mathord {\textnormal {\textsf {e}}}_{a},A):\mathcal {S}(X,0)\rightarrow \mathcal {U}(0)\) has a right adjoint. Such an object is sometimes called tiny.
Let \(T\) be a base type theory. We work in \(T\). Let \(X_{1}\) and \(X_{2}\) be toposes and let \(f:X_{1}\rightarrow X_{2}\) be a morphism. If \(f\) has a right adjoint, then \(f\) is essential.
Proof
This is because the operation \(X\mapsto \mathcal {S}(X,i)\) is \(2\)-functorial and reverses \(1\)-cells.
Let \(T\) be a base type theory. We work in \(T\). Let \(X_{1}\) be a topos and let \(X_{2}:X_{1}\rightarrow \mathcal {E}(0)\). Then the first projection \((x:X_{1})\times X_{2}(x)\rightarrow X_{1}\) is essential.
Proof
Using [002Y], the claim is reduced to the case when \(X_{1}\) is the terminal topos. It is thus enough to show that \(\Delta _{X}:\mathcal {U}(0)\rightarrow \mathcal {S}(X,0)\) has a left adjoint for every \(X:\mathcal {E}(0)\). Let \(A:\mathcal {U}(0)\) correspond to \(X\) by [002S]. By [004W], \(\Delta _{X}\) is equivalent to the constant-function functor \(\mathcal {U}(0)\rightarrow (A\rightarrow \mathcal {U}(0))\). It has the left adjoint \(B\mapsto (x:A)\times B(x)\).
The author does not know a standard name for the following concept, but it gives a nice sufficient condition for a point to be essential.
Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(X\) be a topos. We say a point \(a:X\) is coétale if the type family \((x:X)\mapsto a\Rightarrow x\) is valued in \(\mathcal {E}(0)\).
Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos and let \(a\) be a point of \(X\). Suppose that \(a\) is coétale. Then \(a\) is essential.
Proof
The morphism \(\_\mapsto a:\mathord {\textnormal {\textsf {1}}}\rightarrow X\) factors as \(\_\mapsto (a,\mathord {\textnormal {\textsf {id}}}):\mathord {\textnormal {\textsf {1}}}\rightarrow (x:X)\times (a\Rightarrow x)\) followed by the first projection \((x:X)\times (a\Rightarrow x)\rightarrow X\). The former is a left adjoint and thus essential by [003R]. The latter is essentialy by [003S] and by the assumption that \(a\) is coétale. Thus, their composite is also essential.
Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos and let \(a\) be a coétale point of \(X\). Then we have a canonical equivalence