<p>So we need to construct a natural transformation <span class="math-container">$\phi : K(I)u^\# \Rightarrow u^*(K(J))$</span>, which are functors from <span class="math-container">$D_J$</span> to <span class="math-container">$E_I$</span>. So for every <span class="math-container">$d \in D_J$</span> we need a morphism <span class="math-container">$K(I)(u^\#(d)) \to u^*(K(J)(d))$</span> in <span class="math-container">$E_I$</span>.</p>

<ol>
<li>Since <span class="math-container">$K(I) \dashv H(I)$</span>, this is equivalent to constructing a morphism <span class="math-container">$u^\#(d) \to H(I)(u^*(K(J)(d)))$</span> in <span class="math-container">$E_J$</span>.</li>
<li>Now since <span class="math-container">$H$</span> is a fibred functor, <span class="math-container">$H(I)(u^*(e)) \cong u^\#(H(J)(e))$</span> for any <span class="math-container">$e$</span> so by composition with this isomorphism it is sufficient to construct a morphism <span class="math-container">$u^\#(d) \to u^\#(H(J)(K(J)(d)))$</span>.</li>
<li><span class="math-container">$u^\#$</span> is a functor so it is sufficient to construct a morphism <span class="math-container">$d \to H(J)(K(J)(d))$</span> </li>
<li>So we can just use the unit of the adjunction <span class="math-container">$K(J) \dashv H(J)$</span>.</li>
</ol>

<p>The whole process is natural since every step is natural.</p>

CC BY-SA 4.0
2019-05-18T19:09:55.077Z
Oh, so that's what Jacobs is talking about in the text directly below the lemma. I tried to reverse engineer that, but I got stuck on the natural isomorphism $()^*≅^{\#}(J)$; I couldn't figure out where it came from, but now I see that it's just an appeal to Cartesianness. Your step-by-step explanation was much easier to follow. Shouldn't H(I)K(I) in steps 2,3,and 4 be H(J)K(J)?
Kevin Clancy
CC BY-SA 4.0
2019-05-18T20:36:12.737Z
Yes, fixed now.
Max New
CC BY-SA 4.0
2019-05-18T13:30:22.700Z
2019-05-18T20:35:13.240Z
2019-05-18T20:35:13.240Z
Max New
<p>I've been reading through Bart Jacobs' "Categorical Logic and Type Theory", and lemma 1.8.9 has me stumped. The lemma is stated as follows:</p>

<hr>

<p>Let <span class="math-container">$p : \mathbb E \to \mathbb B$</span> and <span class="math-container">$q : \mathbb D \to \mathbb B$</span> be fibrations and let <span class="math-container">$H : \mathbb E \to \mathbb D$</span> be a fibred functor. This functor <span class="math-container">$H$</span> has a fibred left adjoint if and only if both</p>

<p>(a) For each object <span class="math-container">$I \in \mathbb B$</span> the functor <span class="math-container">$H_I : \mathbb E_I \to \mathbb D_I$</span> restricted to the fibres over <span class="math-container">$I$</span> has a left adjoint <span class="math-container">$K(I)$</span></p>

<p>(b) The <strong>Beck-Chevalley Condition</strong> holds, i.e. for every map <span class="math-container">$u : I \to J$</span> in <span class="math-container">$\mathbb B$</span> and for every pair of reindexing functors <span class="math-container">$\mathbb E_J \overset{u^*}{\longrightarrow} \mathbb E_I$</span> and <span class="math-container">$\mathbb D_J \overset{u^\#}{\longrightarrow} \mathbb D_I$</span>, the canonical natural transformation <span class="math-container">$K(I)u^\# \Rightarrow u^* K(J)$</span>
is an isomorphism.</p>

<hr>

<p>What does the <em>canonical natural transformation</em> <span class="math-container">$K(I)u^\# \Rightarrow u^* K(J)$</span> refer to? I was having a lot of fun reading this book. However, since the Beck-Chevalley condition is used throughout the rest of the book, this particular lemma has become a road block. </p>

<p>I'm not sure if this is considered a research level question, but I don't know where else to ask this.</p>

<ct.category-theory>
Understanding the Beck-Chevalley Condition
Kevin Clancy
# Understanding the Beck-Chevalley Condition

(Asked by: username_0 on 2019-05-17)

I've been reading through Bart Jacobs' "Categorical Logic and Type Theory", and lemma 1.8.9 has me stumped. The lemma is stated as follows:

---

Let $p : \mathbb E \to \mathbb B$ and $q : \mathbb D \to \mathbb B$ be fibrations and let $H : \mathbb E \to \mathbb D$ be a fibred functor. This functor $H$ has a fibred left adjoint if and only if both

(a) For each object $I \in \mathbb B$ the functor $H\_I : \mathbb E\_I \to \mathbb D\_I$ restricted to the fibres over $I$ has a left adjoint $K(I)$

(b) The **Beck-Chevalley Condition** holds, i.e. for every map $u : I \to J$ in $\mathbb B$ and for every pair of reindexing functors $\mathbb E\_J \overset{u^\*}{\longrightarrow} \mathbb E\_I$ and $\mathbb D\_J \overset{u^\#}{\longrightarrow} \mathbb D\_I$, the canonical natural transformation $K(I)u^\# \Rightarrow u^\* K(J)$
is an isomorphism.

---

What does the *canonical natural transformation* $K(I)u^\# \Rightarrow u^\* K(J)$ refer to? I was having a lot of fun reading this book. However, since the Beck-Chevalley condition is used throughout the rest of the book, this particular lemma has become a road block.

I'm not sure if this is considered a research level question, but I don't know where else to ask this.

**Tags:** ct.category-theory

---

## 1 answers

### Answer by username_1 on 2019-05-18. Score: 7 | Accepted answer

So we need to construct a natural transformation $\phi : K(I)u^\# \Rightarrow u^\*(K(J))$, which are functors from $D\_J$ to $E\_I$. So for every $d \in D\_J$ we need a morphism $K(I)(u^\#(d)) \to u^\*(K(J)(d))$ in $E\_I$.

1. Since $K(I) \dashv H(I)$, this is equivalent to constructing a morphism $u^\#(d) \to H(I)(u^\*(K(J)(d)))$ in $E\_J$.
2. Now since $H$ is a fibred functor, $H(I)(u^\*(e)) \cong u^\#(H(J)(e))$ for any $e$ so by composition with this isomorphism it is sufficient to construct a morphism $u^\#(d) \to u^\#(H(J)(K(J)(d)))$.
3. $u^\#$ is a functor so it is sufficient to construct a morphism $d \to H(J)(K(J)(d))$
4. So we can just use the unit of the adjunction $K(J) \dashv H(J)$.

The whole process is natural since every step is natural.

> **Comments:**
> **username_0**: Oh, so that's what Jacobs is talking about in the text directly below the lemma. I tried to reverse engineer that, but I got stuck on the natural isomorphism $()^*≅^{\#}(J)$; I couldn't figure out where it came from, but now I see that it's just an appeal to Cartesianness. Your step-by-step explanation was much easier to follow. Shouldn't H(I)K(I) in steps 2,3,and 4 be H(J)K(J)?  
> **username_1**: Yes, fixed now.  

---

