6
$\begingroup$

Let $F : \mathcal X \to \mathcal A$ be a cloven fibration and let the following be a pullback square in $\mathcal A$:

$$\newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} \newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}} \begin{array}{c} A & \ra{f} & B\\ \da{a} & & \da{b}\\ A' & \ras{f'} & B'\\ \end{array} %this is borrowed from http://meta.math.stackexchange.com/questions/2324/how-to-draw-a-commutative-diagram$$

Then, according for example to B. Jacobs "Categorical Logic and Type Theory" and other sources, the square has the Beck-Chevalley property if 'the canonical natural transformation $\Sigma_f \circ a^* \to b^*\circ \Sigma_{f'}$ is an isomorphism'. Here $f^*$ ($\Sigma_f$) is (co-) reindexing along $f$. This property comes up in the definition of "$F$ has coproducts".

What is this canonical natural transformation explicitly?

Apparently, this is blatantly obvious but I don't see it.

$\endgroup$

1 Answer 1

6
$\begingroup$

The nLab page on the Beck-Chevalley condition is good. The pieces of data we need are that $\Sigma_f \dashv f^*$ and similarly $\Sigma_{f'} \dashv f'^*$. Ignoring that the above commutative diagram is a pullback diagram, we get from it $$\require{AMScd} \begin{CD} \mathcal{X}_A @<f^*<< \mathcal{X}_B \\ @Aa^*A\qquad \cong A @AAb^*A \\ \mathcal{X}_{A'} @<<f'^*< \mathcal{X}_{B'} \end{CD}$$ which commutes up to isomorphism. This can be viewed as a square in the double category of adjunctions, and, as the Beck-Chevalley page states, the notion of mates (or conjugates) gives exactly the "canonical transformation" given the above diagram. Explicitly, this is the arrow $$\begin{CD} \Sigma_f \circ a^* @>\Sigma_fa^*\eta>> \Sigma_f \circ a^*\circ f'^*\circ \Sigma_{f'}@>\cong>> \Sigma_f\circ f^*\circ b^*\circ\Sigma_{f'} @>\varepsilon_{b^*\Sigma_{f'}}>> b^* \circ \Sigma_{f'} \end{CD}$$ where the $\eta$ is the unit of the $\Sigma_{f'}\dashv f'^*$ adjunction and the $\varepsilon$ is the counit of the $\Sigma_f \dashv f^*$ adjunction. All of this applies for arbitrary adjunctions in an arbitrary 2-category. The Beck-Chevalley condition simply states that if the above (pseudo-)commutative square is the image of a pullback square, then the above natural transformation is an isomorphism.

The nLab page also has a good description of what the Beck-Chevalley condition means in a logic/type theory context, namely that substitution commutes with dependent sum formation.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .