[003J] Direct images

A morphism between toposes also induces the direct image functor which is a right adjoint of the inverse image functor. The construction of the direct image functor is not so straightforward as that of the inverse image functor. We first define a special case, the global section functor, and then relativize it using [002Y].

[003K] Definition

Let $$T$$ be a type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $$X$$ be a topos. We define the global section functor

\Gamma _{X}:\mathcal {S}(X,i)\rightarrow \mathcal {U}(i)

by the following composite.

\mathcal {S}(X,i)

\simeq

{[003G]}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}({}\vdash \mathcal {U}(i))

\rightarrow

{

\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}

}

\mathcal {U}(i)

By [002R],

\Gamma _{X}

has a left adjoint which we call the constant sheaf functor and is denoted by

\Delta _{X}

[003N] Observation

Let $$T$$ be a base type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $X_{1}$ be a topos, and let $X_{2}(x)$ be a topos under assumption $x:X_{1}$ . Then we have the following equivalences.

\mathcal {S}((x:X_{1})\times X_{2}(x),i)

\simeq

{[002Y]}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{1})}(\mathord {\textnormal {\textsf {Sp}}})}(y:X_{2}(\mathord {\textnormal {\textsf {w}}}_{X_{1}})\vdash \mathcal {E}(i))

\simeq

{definition}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{1})}({}\vdash \mathcal {S}(X_{2}(\mathord {\textnormal {\textsf {w}}}_{X_{1}}),i))

[003L] Definition

{f}_{*}:\mathcal {S}(X_{1},i)\rightarrow \mathcal {S}(X_{2},i)

by the following composite.

\mathcal {S}(X_{1},i)

\simeq

{fibrant replacement}

\mathcal {S}((y:X_{2})\times \mathord {\textnormal {\textsf {Fib}}}(f,y),i)

\simeq

{[003L]}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{2})}({}\vdash \mathcal {S}(\mathord {\textnormal {\textsf {Fib}}}(f,\mathord {\textnormal {\textsf {w}}}_{X_{2}}),i))

\rightarrow

{

\Gamma _{\mathord {\textnormal {\textsf {Fib}}}(f,\mathord {\textnormal {\textsf {w}}}_{X_{2}})}

}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{2})}({}\vdash \mathcal {U}(i))

\simeq

{[003G]}

\mathcal {S}(X_{2},i)

[003M] Exercise

Let $$T$$ be a base type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $X_{1}$ and $X_{2}$ be toposes, and let $f:X_{1}\rightarrow X_{2}$ be a morphism. Then ${f}_{*}:\mathcal {S}(X_{1},i)\rightarrow \mathcal {S}(X_{2},i)$ is a right adjoint of ${f}^{*}:\mathcal {S}(X_{2},i)\rightarrow \mathcal {S}(X_{1},i)$ .