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)$.
- the unit-counit adjunction
- adjunctions by universal morphisms
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).
