7
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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)? $\endgroup$ – Kevin Clancy May 18 at 19:09
  • $\begingroup$ Yes, fixed now. $\endgroup$ – Max New May 18 at 20:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.