Understanding the Beck-Chevalley condition

Question

Having opened the black box of Beck's monadicity theorem, I would now like to do the same for monadic descent. While probing around I keep encountering the Beck-Chevalley condition.

Unfortunately, the nlab entry is way above my head. I want to understand the intuitive idea behind this condition in some concrete cases but I don't even know how to start.

What is the intuitive meaning of the Beck-Chevalley condition, either from a geometric perspective or from a logical one? (I don't know type theory.)

Answer 1

$\require{AMScd}$ When you do algebraic geometry, you can consider diagrams like $$ \begin{CD} X @>f>> A\\ @VgVV \\ B \end{CD} $$ where $X,A,B$ are spaces and $g,f$ maps thereof. It is fairly natural to think these as "generalized functions" between $A$ and $B$. They are in fact called "correspondences" between $A$ and $B$, and they organize in a category that contains your category of spaces in (actually two) canonical way(s).

Morally, these guys correspond to "pull-push" functors like $g_*f^* : D(A)\to D(B)$. But there is a subtlety: in order for this to be a well-defined (bi)category, you must specify coherence conditions on a composition law: the most natural thing to do, given a diagram $$ \begin{CD} @. X @>f>> A\\ @. @VgVV \\ Y @>h>> B\\ @VkVV\\ C \end{CD} $$ is to complete it to a pullback $$ \begin{CD} P @>q>> X @>f>> A\\ @VpVV @VgVV \\ Y @>h>> B\\ @VkVV\\ C \end{CD} $$ Notice that you have two seemingly different ways to read your composition, now: the first, as $(kp)_*(fq)^* = k_* p_* q^* f^*$ and the second as $k_* h^* g_* f^*$. When will these two be equal (or rather, canonically isomorphic)?

Answer 2

The nLab page has a decent discussion about the logical perspective. The beginning of Dusko Pavlovic's 1996 paper Maps II: Chasing Diagrams in Categorical Proof Theory has a fairly readable description of the situation too. The below is a significantly elaborated form of the example from that paper.

Before that, I want to point out a different perspective that is discussed in section 3 and particularly proposition 3.4 of Bart Jacobs' Comprehension categories and the semantics of type dependency. We have a 2-category of fibrations over a base category (which is itself a fiber in fibration of fibrations). We thus can instantiate the 2-categorical definition of adjunction to it. The result is a fibred adjunction which is a (normal) adjunction of cartesian functors between the total categories whose unit (or equivalently counit) is vertical which induces an adjunction in each fiber which is preserved by reindexing. The obvious question is: when does a collection of fiberwise left/right adjoints to fibers of a cartesian functor give rise to a fibred left/right adjoint? The answer is: exactly when the (generalized) Beck-Chevalley condition holds.

Let $\pi_! \dashv \pi^*$ where $\pi^*$ is the inverse image of projection, called the weakening functor, and $\pi_!$ is the direct image and corresponds to existential quantification, i.e. $\pi_{!,B}(x:A,y:B\vdash P(x,y))$ corresponds to $x:A\vdash\exists y:B.P(x,y)$. The inverse image $\pi_B^*(x:A\vdash P(x))$ corresponds to $x:A,y:B\vdash P(x)$, hence "weakening". Now the problem is there are two ways to get $x:A\vdash \exists y:B.R(\sigma(x),y)$ starting from $x:A,y:B\vdash R(x,y)$. You could first existentially quantify getting $x:A\vdash\exists y:B.R(x,y)$ and then substitute, or you could first substitute $x:A,y:B\vdash R(\sigma(x),y)$ and then existentially quantify. The pullback square in the base is $$\require{AMScd} \begin{CD} A\stackrel{\times}{{}_{\pi_B,\sigma}} B @>\hat\pi_B>> A\\ @V\hat\sigma VV @VV\sigma V \\ A\times B @>\pi_B>> A \end{CD}$$ and we get $\hat\pi_{!,B}\circ\hat\sigma^* \to \sigma^*\circ\pi_{!,B}$. The natural transformation arises as described here and in this case looks like $$\cfrac{\cfrac{ x:A\vdash\exists y:B.[\sigma(x)/x,y/y]_{x,y}R(x,y)} {x:A\vdash\exists y:B.[\sigma(x)/x,y/y]_{x,y}[x/x]_{x,y}\exists w:B.R(x,w)}}{ \cfrac{x:A\vdash \exists y:B.[x/x]_{x,y}[\sigma(x)/x]_{x}\exists w:B.R(x,w)}{ x:A\vdash[\sigma(x)/x]_{x}\exists w:B.R(x,w)}}$$ where I'm using e.g. $[\sigma(x)/x]_{x,y}$ as a substitution replacing $x$ with $\sigma(x)$ in terms of the variables $x$, and $y$. That the above implication should be an equivalence is the Beck-Chevalley condition.