Constructing pointwise Kan extensions as adjoints to some functor

Background

I'm working on formalizing some category theory in Coq at https://bitbucket.org/JasonGross/catdb. Currently, I'm in the process of formalizing pointwise Kan extensions. Partly because I'm running into speed problems with constructions involving extensive use of comma categories, and partly because I like elegance, I'd like to factor out the construction into some general pieces, and obtain the construction by composing these pieces.

Goal

Let $\mathcal C$, $\mathcal D$, and $\mathcal E$ be categories, and let $F : \mathcal D \to \mathcal E$ be a functor. Define $\Delta_F : \mathcal C^{\mathcal E} \to \mathcal C^{\mathcal D}$ be the functor $\text{Hom}_\text{Cat}(-, F)$. Assuming that $\mathcal C$ has all (co)limits of the appropriate shapes, I want to prove that $\Delta_F$ has left and right adjoints $\Sigma_F$ and $\Pi_F$.

I'm pretty sure that these are called left and right Kan extensions, I believe the shapes are $d \downarrow F$ for limits and $F \downarrow d$ for colimits, for all $d \in \text{Ob}(\mathcal D)$, which are comma categories, and I believe that the assumption that the limits and colimits exist means that I'm attempting to construct the Kan extensions pointwise.

I am interested in a "high level" construction of these functors, i.e., one where I get that $\Pi_F$ and $\Sigma_F$ are adjoints to $\Delta_F$ "for free", simply as a result of the construction.

Setup (what I have so far)

I have formalized the following bits of category theory, which I believe might be relevant to such a construction. (Alternatively, I am looking for a construction which builds on these bits of category theory in a suitably nice way.)

• I have limit and colimit functors defined as adjoints to the constant diagram functor. More formally: Let $\mathcal C$ and $\mathcal D$ be categories, and let $\Delta : \mathcal C \to \mathcal C^{\mathcal D}$ be the constant diagram functor (which sends objects $c$ to the functor which, on morphisms, is $(s \xrightarrow{m} d) \mapsto (c \xrightarrow{\text{id}} c)$). Suppose $\mathcal C$ has all $\mathcal D$-shaped limits and colimits. Then we have that $\Delta$ has adjoints $\text{lim} : \mathcal C^{\mathcal D} \to \mathcal C$ and $\text{colim} : \mathcal C^{\mathcal D} \to \mathcal C$.
• I have equivalent formulations of adjoint functors $F : \mathcal C \leftrightarrows \mathcal D : G$:

• the hom-set/natural isomorphism definition: there exists a natural isomorphism $\text{Hom}_{\mathcal D}(F -, -) \cong \text{Hom}_{\mathcal C}(-, G -)$
• the universal property of the unit (Awodey's Category Theory, Proposition 9.4): There is a natural transformation $\eta : 1_{\mathcal C} \to G \circ F$ such that for any $c \in \mathcal C$, $d \in \mathcal D$, and $f : c \to G(d)$, there exists a unique $g : F(c) \to d$ such that $f = G(g) \circ \eta_c$.
• the universal property of the counit (Awodey's Category Theory, Corollary 9.5): There is a natural transformation $\epsilon : F \circ G \to 1_{\mathcal D}$ such that for any $c \in \mathcal C$, $d \in \mathcal D$, and $g : F(c) \to d$, there exists a unique $f : c \to G(d)$ such that $g = \epsilon_d \circ F(f)$.
• I have proven that adjoints compose. That is, given $F : \mathcal C \rightleftarrows \mathcal D : G$ and $F' : \mathcal D \rightleftarrows \mathcal E : G'$, with $F \dashv G$ and $F' \dashv G'$, I have constructed the adjunction $F' \circ F : \mathcal C \rightleftarrows \mathcal E : G' \circ G$.

• I have constructed adjoints pointwise. That is, given $F : \mathcal C \rightleftarrows \mathcal D : G$ with $F \dashv G$, and given a category $\mathcal E$, I have constructed the adjunction $F^{\mathcal E} : \mathcal C^{\mathcal E} \rightleftarrows \mathcal D^{\mathcal E} : G^{\mathcal E}$. (I'm not sure if this is the standard notation. Perhaps I should be saying, e.g., $F^{1_{\mathcal E}}$ for the functor $\text{Hom}_{\text{Cat}}(F, 1_{\mathcal E})$?) (As an aside, I feel like I might be able to generalize this, so that I can pick different exponents for $\mathcal C$ and $\mathcal D$, but I'm not sure how, or even if it's possible.)

• I know that the constant diagram functor $\Delta$ comes from $\Delta_F : \mathcal C^{\mathcal E} \to \mathcal C^{\mathcal D}$ by taking $\mathcal E = 1$ to be the terminal category and taking $F$ to be the unique functor $\mathcal D \to 1$.

Contextualized Goal

Given this setup, I'd like a construction of adjoints to $\Delta_F$ which doesn't talk about $\Delta_F$ until the very end. That is, I would like to construct some more properties of adjoints (maybe involving comma categories), compose some adjoints, and then say "when you plug in $\Delta_F$ here, and you plug in the fact that we have enough universal morphisms that $\Delta$ has adjoints there, then out pops the fact that $\Delta_F$ has adjoints". (I'm fine with having to generalize adjoints to weighted adjoints, or multi-variable adjunctions, or whatever the equivalent of adjoints are when comma categories are replaced by (op)lax comma categories, or something like that.) I feel that I should be able to do this because I was able to do a similar thing to prove that lim and colim are functors: a functor is a left adjoint (has a right adjoint) whenever all of the appropriate terminal morphisms exist (as per http://en.wikipedia.org/wiki/Adjoint_functor#Universal_morphisms), and a limit is just a terminal morphism of $\Delta$, and thus if all appropriately shaped limits exist, the limit objects assemble into a limit functor which is adjoint to $\Delta$.

I think another way of stating this, using the universal morphism construction of adjoints, is that I'm looking to prove the following goal:

Given the following context:

• categories $\mathcal C$, $\mathcal D$, and $\mathcal E$
• a functor $F : \mathcal D \to \mathcal E$
• for all $d \in \text{Ob}(\mathcal D)$ and all functors $G : {d \downarrow F} \to \mathcal C$, we have a terminal object of the category $\Delta \downarrow G$ (where $\Delta$ is the constant diagram functor $\mathcal C \to \mathcal C^{d \downarrow F}$)

I want to construct, for all functors $H : \mathcal D \to \mathcal C$, a terminal object of the category $\Delta_F \downarrow H$. I want to do this construction in a way that gives me the fact that my construction is a terminal object "for free" (see above).

-
The adjoints of $\Delta_F$ are what Kelly calls weak Kan extensions, i.e. the not-necessarily-pointwise Kan extensions. If you want pointwiseness you have to demand that certain commutative squares satisfy the Beckâ€“Chevalley condition. – Zhen Lin Mar 18 '13 at 7:48
Thanks. I've removed "pointwise" from the question. I think I had called them pointwise because I was misremembering a suggestion that I heard, which I think was actually a suggestion that this construction might be similar to a construction of pointwise Kan extensions. – Jason Gross Mar 18 '13 at 13:02
Does assuming that all limits and colimits of the appropriate shape exist imply that the Kan extensions are necessarily pointwise? If so, what I'm trying to construct here are pointwise Kan extensions. – Jason Gross Mar 20 '13 at 16:18
@Jason Gross once you have all limits and colimits of the appropriate shape, then your Kan extensions are pointwise. This is in Categories for the Working Mathematician X.5.3, but I learned it from these notes of Emily Riehl: math.harvard.edu/~eriehl/266x/lectures.pdf – John Wiltshire-Gordon Mar 20 '13 at 17:01
@Jason What John said, but with the proviso that the diagrams involved can be large if $\mathcal{D}$ is large. The usual statement is, if $\mathcal{C}$ has limits/colimits for all small diagrams, $\mathcal{D}$ is small, and $\mathcal{E}$ is locally small, then for all functors $F : \mathcal{D} \to \mathcal{E}$ and all functors $H : \mathcal{D} \to \mathcal{C}$, the right/left Kan extension of $H$ along $F$ exists and is pointwise. – Zhen Lin Mar 20 '13 at 20:40