nLab Beck-Chevalley condition




The BeckChevalley condition, also sometimes called just the Beck condition or the Chevalley condition, is a “commutation of adjoints” property that holds in many “change of base” situations.


The Beck-Chevalley condition may be understood as a natural compatibility condition for

(1) integral transforms in geometry

(2) quantifiers in formal logic/type theory

From integral transforms

From the point of view of geometry, in contexts such as of integral transforms one considers correspondences between spaces AA, BB given by spans of maps between them:

Via composition of such correspondences by fiber product of adjacent legs, they form the 1-morphisms in a 2-category Span.

Assuming some base change adjoint pair f *f *f^\ast \vdash f_\ast, thought of as

  • push-forward f *:𝒟(X)𝒟(A)f_\ast \,\colon\, \mathcal{D}(X) \longrightarrow \mathcal{D}(A)


  • pull-back f *:𝒟(A)𝒟(X)f^\ast \,\colon\, \mathcal{D}(A) \longrightarrow \mathcal{D}(X)

is functorially associated with maps ff (i.e. such that there are natural isomorphisms (f 2f 1) *(f 2) *(f 1) *(f_2 f_1)_\ast \,\simeq\, (f_2)_\ast (f_1)_\ast and dually), the integral transform encoded by any span as above is the “pull-push” operation given by g *f *g_* f^*.

Now the Beck-Chevalley condition (on such assignment of base change adjoints to maps) essentially says that this pull-push construction is (2-)functorial under composition of spans:

Concretely, given a pair of composable spans:

and their composite in Span formed by the fiber product of the adjacent legs

then functoriality of pull-push means that the two different ways to pull-push through the diagram coincide:

Pull-pushing through the spans separately results in

(k *h *)(g *f *)=k *h *g *f *, (k_\ast h^\ast) \circ (g_\ast f^\ast) \;=\; k_\ast \, \underbrace{h^\ast \, g_\ast} \, f^\ast \,,

while pull-pushing through the composite span results in

(kp) *(fq) *=k *p *q *f *. (k p)_* (f q)^* = k_* \, \underbrace{p_* \, q^*} \, f^* \,.

For these two operations to coincide, up to isomorphism, hence for pull-push to respect composition of spans, we need an isomorphism between the operations shown over braces, hence of the form

(1)h *g *p *q * h^\ast \, g_\ast \;\simeq\; p_* \, q^*

between the two ways of push-pulling along the sides of any pullback square

This (1) is the Beck-Chevalley condition: A natural necessary condition to ensure that integral transforms by pull-push base change through correspondences is functorial under composition of correspondences by fiber product of adjacent legs.

More motivation along these lines also be found at dependent linear type theory. As a formulation of propagation in cohomological quantum field theory this is Sc14 there.

From logic and type theory

From the point of view of formal logic and dependent type theory, the three items f !f *f *f_! \dashv f^\ast \vdash f_\ast in a base change adjoint triple constitute the categorical semantics of quantification and context extension (existential quantification/dependent pair type \dashv context extension \dashv universal quantification/dependent product type), and so the Beck-Chevalley condition says that these are compatible with each other: concretely that substitution of free variables commutes with quantification — a condition which syntactically is “self-evident”, at least it is evidently desirable.

For more on this logical aspect see below.


Suppose given a commutative square (up to isomorphism) of functors:

f * g * k * h * \array{ & \overset{f^*}{\to} & \\ ^{g^*}\downarrow && \downarrow^{k^*}\\ & \underset{h^*}{\to} & }

in which f *f^* and h *h^* have left adjoints f !f_! and h !h_!, respectively. (The classical example is a Wirthmüller context.) Then the natural isomorphism that makes the square commute

k *f *h *g * k^* f^* \to h^* g^*

has a mate

h !k *g *f ! h_! k^* \to g^* f_!

defined as the composite

h !k *ηh !k *f *f !h !h *g *f !ϵg *f !. h_! k^* \overset{\eta}{\to} h_! k^* f^* f_! \overset{\cong}{\to} h_! h^* g^* f_! \overset{\epsilon}{\to} g^* f_! \,.

We say the original square satisfies the Beck–Chevalley condition if this mate is an isomorphism.

More generally, it is clear that for this to make sense, we only need a transformation k *f *h *g *k^* f^* \to h^* g^*; it doesn’t need to be an isomorphism. We also use the term Beck–Chevalley condition in this case,

Left and right Beck–Chevalley condition

Of course, if g *g^* and k *k^* also have left adjoints, there is also a Beck–Chevalley condition stating that the corresponding mate k !h *f *g !k_! h^* \to f^* g_! is an isomorphism, and this is not equivalent in general. Context is usually sufficient to disambiguate, although some people speak of the “left” and “right” Beck–Chevalley conditions.

Note that if k *f *h *g *k^* f^* \to h^* g^* is not an isomorphism, then there is only one possible Beck-Chevalley condition.

Dual Beck–Chevalley condition

If f *f^* and h *h^* have right adjoints f *f_* and h *h_*, there is also a dual Beck–Chevalley condition saying that the mate g *f *h *k *g^* f_* \to h_* k^* is an isomorphism. By adjointness, if f *f^* and h *h^* have right adjoints and g *g^* and k *k^* have left adjoints, then g *f *h *k *g^* f_* \to h_* k^* is an isomorphism if and only if k !h *f *g !k_! h^* \to f^* g_! is.

For bifibrations

Originally, the Beck-Chevalley condition was introduced in (Bénabou-Roubaud, 1970) for bifibrations over a base category with pullbacks. In loc.cit. they call this condition Chevalley condition because he introduced it in his 1964 seminar.

A bifibration XB\mathbf{X} \to \mathbf{B} where B\mathbf{B} has pullbacks satisfies the Chevalley condition iff for every commuting square

ψ φ φ ψ \array{ & \overset{\psi^\prime}{\rightarrow} & \\ \downarrow^{\varphi^\prime} && \downarrow^{\varphi}\\ & \underset{\psi}{\rightarrow} & }

in X\mathbf{X} over a pullback square in the base B\mathbf{B} where φ\varphi is cartesian and ψ\psi is cocartesian it holds that φ \varphi^\prime is cartesian iff ψ \psi^\prime is cocartesian. Actually, it suffices to postulate one direction because the other one follows. The nice thing about this formulation is that there is no mention of “canonical” morphisms and no mention of cleavages.

A fibration PP has products satisfying the Chevalley condition iff the opposite fibration P opP^{op} is a bifibration satisfying the Chevalley condition in the above sense.

According to the Benabou–Roubaud theorem, the Chevalley condition is crucial for establishing the connection between the descent in the sense of fibered categories and the monadic descent.

“Local” Beck–Chevalley condition

Suppose that f *f^* and h *h^* do not have entire left adjoints, but that for a particular object xx the left adjoint f !(x)f_!(x) exists. This means that we have an object “f !xf_! x” and a morphism η x:xf *f !x\eta_x\colon x \to f^* f_! x which is initial in the comma category (x/f *)(x / f^*). Then we have k *(η):k *xk *f *f !xh *g *f !xk^*(\eta) \colon k^* x \to k^* f^* f_! x \to h^* g^* f_! x, and we say that the square satisfies the local Beck-Chevalley condition at xx if k *(η)k^*(\eta) is initial in the comma category (k *x/h *)(k^* x / h^*), and hence exhibits g *f !xg^* f_! x as “h !k *xh_! k^* x” (although we have not assumed that the entire functor h !h_! exists).

If the functors f !f_! and h !h_! do exist, then the square satisfies the (global) Beck-Chevalley condition as defined above if and only if it satisfies the local one defined here at every object.

In logic / type theory

If the functors in the formulation of the Beck-Chevalley condition are base change functors in the categorical semantics of some dependent type theory (or just of a hyperdoctrine) then the BC condition is equivalently stated in terms of logic as follows.

A commuting diagram

D h C k g A f B \array{ D &\stackrel{h}{\to}& C \\ {}^{\mathllap{k}}\downarrow && \downarrow^{\mathrlap{g}} \\ A &\stackrel{f}{\to}& B }

is interpreted as a morphism of contexts. The pullback (of slice categories or of fibers in a hyperdoctrine) h *h^* and f *f^* is interpreted as the substitution of variables in these contexts. And the left adjoint kk !\sum_k \coloneqq k_! and qg !\sum_q \coloneqq g_!, the dependent sum is interpreted (up to (-1)-truncation, possibly) as existential quantification.

In terms of this the Beck-Chevalley condition says that if the above diagram is a pullback, then substitution commutes with existential quantification

kh *ϕf * gϕ. \sum_k h^* \phi \stackrel{\simeq}{\to} f^* \sum_g \phi \,.

Consider the diagram of contexts

[Γ,x:X] [Γ,x:X,y:Y] Γ [Γ,y:Y]Γ×X (p 1,p 2,t) Γ×X×Y p 1 (p 1,p 3) Γ (id,t) Γ×Y, \array{ [\Gamma, x : X] &\stackrel{}{\to}& [\Gamma, x : X, y : Y] \\ \downarrow && \downarrow \\ \Gamma &\to& [\Gamma, y : Y] } \;\;\; \simeq \;\;\; \array{ \Gamma \times X &\stackrel{(p_1,p_2,t)}{\to}& \Gamma \times X \times Y \\ {}^{\mathllap{p_1}}\downarrow && \downarrow^{\mathrlap{(p_1,p_3)}} \\ \Gamma &\stackrel{(id,t)}{\to} & \Gamma \times Y } \,,

with the horizontal morphism coming from a term t:ΓYt : \Gamma \to Y in context Γ\Gamma and the vertical morphisms being the evident projection, then the condition says that we may in a proposition ϕ\phi substitute tt for yy before or after quantifying over xx:

x:Xϕ(x,t)( x:Xϕ(x,y))[t/y]. \sum_{x : X} \phi(x,t) \simeq (\sum_{x : X} \phi(x,y))[t/y] \,.



For categories of presheaves


If ϕ:DC\phi : D \to C is an opfibration of small categories and

D β D ψ ϕ C α C \array{ D' &\stackrel{\beta}{\to}& D \\ \downarrow^{\mathrlap{\psi}} && \downarrow^{\mathrlap{\phi}} \\ C' &\stackrel{\alpha}{\to}& C }

is a pullback diagram (in the 1-category Cat), and for 𝒞\mathcal{C} a category with all small colimits, then the induced diagram of presheaf categories

[D,𝒞] β * [D,𝒞] ψ * ϕ * [C,𝒞] α * [C,𝒞], \array{ [D', \mathcal{C}] &\stackrel{\beta^*}{\longleftarrow}& [D, \mathcal{C}] \\ \uparrow^{\mathrlap{\psi}^*} && \uparrow^{\mathrlap{\phi}^*} \\ [C', \mathcal{C}] &\stackrel{\alpha^*}{\longleftarrow}& [C,\mathcal{C}] } \,,

satisfies the Beck-Chevalley condition: for ψ !\psi_! and ϕ !\phi_! denoting the left Kan extension along ψ\psi and ϕ\phi, respectively, then we have a natural isomorphism

ψ !β *α *ϕ !. \psi_! \beta^* \simeq \alpha^* \phi_! \,.

(This is maybe sometimes called the projection formula. But see at projection formula.)

For this statement in the more general context of quasicategories see Joyal 2008, prop. 11.6.


Since ϕ\phi is opfibered, for every object cCc \in C the embedding of the fiber ϕ 1(c)\phi^{-1}(c) into the comma category ϕ/c\phi/c is a final functor. Therefore the pointwise formula for the left Kan extension ϕ !\phi_! is equivalently given by taking the colimit over the fiber, instead of the comma category

ϕ 1(X) clim ϕ 1(c)X. \phi_1(X)_c \simeq \lim_{\underset{\phi^{-1}(c)}{\to}} X \,.

Therefore we have a sequence of isomorphisms

(ψ !β *X)(c) lim ψ 1(c)(Xβ) lim ϕ 1(α(c))X (α *ϕ !X)(c) \begin{aligned} (\psi_! \beta^* X)(c') & \simeq \lim_{\underset{\psi^{-1}(c')}{\to}} (X\circ \beta) \\ & \simeq \lim_{\underset{\phi^{-1}(\alpha(c'))}{\to}} X \\ & \simeq (\alpha^* \phi_! X)(c') \end{aligned}

all of them natural in cc'.

For an example that prop. may fail without the condition that DCD \to C is an opfibration:

Consider C=C= the interval category (01)(0\to 1), D=C=D=C'= the terminal category, ϕ=0\phi=0, α=1\alpha=1, so that D=D'=\emptyset, but α *ϕ !\alpha^*\phi_! is the identity functor.

Proper base change in étale cohomology

For coefficients of torsion group, étale cohomology satisfies Beck-Chevalley along proper morphisms. This is the statement of the proper base change theorem. See there for more details.

Grothendieck six operations

A kind of Beck-Chevalley condition appears in the axioms of Grothendieck’s six operations. See there for more.


The Beck-Chevalley condition has arisen in the theory of descent - as developed from Grothendieck 1959. Jon Beck and Claude Chevalley studied it independently from each another. […] It is conspicuous that neither of them ever published anything on it. [Pavlović 1991, §14]

Original articles:


and in the generality of \infty -categories:

Discussion for subobject lattices:

Discussion for presheaf categories in the context of quasicategories ( \infty -categories of \infty -presheaves):

Discussion for Goursat categories:

Last revised on January 22, 2023 at 12:01:45. See the history of this page for a list of all contributions to it.