For $f : X \to Y$ a morphism in a category $C$ with pullbacks, there is an induced functor
of over-categories. This is the base change morphism. If $C$ is a topos, then this refines to an essential geometric morphism
The dual concept is cobase change.
For $f : X \to Y$ a morphism in a category $C$ with pullbacks, there is an induced functor
of over-categories. It is on objects given by pullback/fiber product along $f$
The concept of base change generalises from this case to other fibred categories.
For $\mathbf{H}$ is a topos (or (∞,1)-topos, etc.) $f : X \to Y$ a morphism in $\mathbf{H}$, then base change induces an essential geometric morphism betwen over-toposes/over-(∞,1)-toposes
where $f_!$ is given by postcomposition with $f$ and $f^*$ by pullback along $f$.
That we have adjoint functors/adjoint (∞,1)-functors $(f_! \dashv f^*)$ follows directly from the universal property of the pullback. The fact that $f^*$ has a further right adjoint is due to the fact that it preserves all small colimits/(∞,1)-colimits by the fact that in a topos we have universal colimits and then by the adjoint functor theorem/adjoint (∞,1)-functor theorem.
The (co-)monads induced by the adjoint triple in prop. 1 have special names in some contexts:
$f_\ast f^\ast$ is also called the function monad (or “reader monad”, see at monad (in computer science)).
in modal type theory $f^\ast f_\ast$ is necessity while $f_! f^\ast$ is possibility.
Here $f^\ast$ is a cartesian closed functor, hence base change of toposes constitutes a cartesian Wirthmüller context.
See at cartesian closed functor for the proof.
$f^*$ is a logical functor. Hence $(f^* \dashv f_*)$ is also an atomic geometric morphism.
This appears for instance as (MacLaneMoerdijk, theorem IV.7.2).
By prop. 1 $f^*$ is a right adjoint and hence preserves all limits, in particular finite limits.
Notice that the subobject classifier of an over topos $\mathbf{H}/X$ is $(p_2 : \Omega_{\mathbf{H}} \times X \to X)$. This product is preserved by the pullback by which $f^*$ acts, hence $f^*$ preserves the subobject classifier.
To show that $f^*$ is logical it therefore remains to show that it also preserves exponential objects. (…)
A (necessarily essential and atomic) geometric morphism of the form $(f^* \dashv \prod_f)$ is called the base change geometric morphism along $f$.
The right adjoint $f_* = \prod_f$ is also called the dependent product relative to $f$.
The left adjoint $f_! = \sum_f$ is also called the dependent sum relative to $f$.
In the case $Y = *$ is the terminal object, the base change geometric morphism is also called an etale geometric morphism. See there for more details
If $\mathcal{C}$ is a locally cartesian closed category then for every morphism $f \colon X \to Y$ in $f$ the inverse image $f^* \colon \mathcal{C}_{/Y} \to \mathcal{C}_{/X}$ of the base change is a cartesian closed functor.
See at cartesian closed functor – Examples for a proof.
Base change geometric morphisms may be interpreted in terms of fiber integration. See integral transforms on sheaves for more on this.
base change
A general discussion that applies (also) to enriched categories and internal categories is in
Discussion in the context of topos theory is around example A.4.1.2 of
and around theorem IV.7.2 in
Discussion in the context of (infinity,1)-topos theory is in section 6.3.5 of
See also