nLab
cartesian closed functor

Definition

Definition

A cartesian closed functor is a functor $F:𝒞\to 𝒟$ between cartesian closed categories which preserves both products and exponential objects/internal homs (all the structure of cartesian closed categories).

More precisely, if $F:C\to D$ preserves products, then the canonical morphisms $F(A\times B)\to FA\times FB$ (for all objects $A,B𝒞$) are isomorphisms, and we therefore have canonical induced morphism $F[A,B]\to [FA,FB]$ — the adjuncts of the composite $F[A,B]\times FA\stackrel{\cong }{\to }F([A,B]\times A)\to FB$. $F$ is cartesian closed if these maps $F[A,B]\to [FA,FB]$ are also isomorphisms.

Remark

When cartesian closed categories are identified with cartesian monoidal categories that are also closed monoidal, a cartesian closed functor can be identified with a strong monoidal functor which is also strong closed.

Properties

Proposition

(Frobenius reciprocity)

Let $R:𝒞\to 𝒟$ be a functor between cartesian closed categories with a left adjoint $L$. Then $R$ is cartesian closed precisely if the natural transformation

$$(L{\pi }_1,{ϵ}_{A}L{\pi }_2):L(B\times R(A))\to L(B)\times A$$(L \pi_1, \epsilon_A L \pi_2) : L(B \times R(A)) \to L(B) \times A

is an isomorphism.

Proof

The above natural transformation is the mate of the exponential comparison natural transformation $R[A,B]\to [RA,RB]$ under the composite adjunctions

$$𝒞\underset{[RA,-]}{\overset{-\times RA}{\rightleftarrows }}𝒞\underset{R}{\overset{L}{\rightleftarrows }}𝒟$$\mathcal{C} \underoverset{[R A, -]}{- \times R A}{\rightleftarrows} \mathcal{C} \underoverset{R}{L}{\rightleftarrows} \mathcal{D}

and

$$𝒞\underset{R}{\overset{L}{\rightleftarrows }}𝒟\underset{[A,-]}{\overset{A\times -}{\rightleftarrows }}𝒟$$\mathcal{C} \underoverset{R}{L}{\rightleftarrows} \mathcal{D} \underoverset{[A,-]}{A\times -}{\rightleftarrows} \mathcal{D}

This is called the Frobenius reciprocity law. It is discussed, for instance, as (Johnstone, lemma 1.5.8).

Let still $R$ and $L$ be as above.

Corollary

If $R$ is full and faithful and $L$ preserves binary products, then $R$ is cartesian closed.

For instance (Johnstone, corollary A1.5.9).

Examples

Proposition

For $𝒞$ a locally cartesian closed category and $f:X_1\to X_2$ a morphism, the base change/pullback functor between the slice categories

$$f^{*}:{𝒞}_{/X_2}\to {𝒞}_{/X_1}$$f^* : \mathcal{C}_{/X_2} \to \mathcal{C}_{/X_1}

is cartesian closed.

In particular the inverse image functor of an étale geometric morphism between toposes is cartesian closed.

Proof

The functor $f^{*}$ has a left adjoint

$$\sum _f:{𝒞}_{/X_1}\to {𝒞}_{/X_2}$$\sum_f : \mathcal{C}_{/X_1} \to \mathcal{C}_{/X_2}

given by postcomposition with $f$ (the dependent sum along $f$). Therefore by prop. 1 it is sufficient to show that for all $(A\to X_2)$ in ${𝒞}_{/X_2}$ and $(B\stackrel{b}{\to }{X}_1)\in {𝒞}_{/X_1}$ that

$$B{\times }_{X_1}{f}^{*}A\simeq B{\times }_{X_2}A$$B \times_{X_1} f^* A \simeq B \times_{X_2} A

in $𝒞$. But this is the pasting law for pullbacks in $𝒞$, which says that the two consecutive pullbacks on the left of

$$\begin{array}{ccccc}B{\times }_{X_1}{f}^{*}A& \to & f^{*}A& \to & A\\ \downarrow & & \downarrow & & \downarrow \\ B& \stackrel{b}{\to }& X_1& \stackrel{f}{\to }& X_2\end{array}\simeq \begin{array}{ccccc}(b\circ f{)}^{*}A& \to & & \to & A\\ \downarrow & & & & \downarrow \\ B& \stackrel{b}{\to }& X_1& \stackrel{f}{\to }& X_2\end{array}$$\array{ B \times_{X_1} f^* A &\to& f^* A &\to& A \\ \downarrow && \downarrow && \downarrow \\ B &\stackrel{b}{\to}& X_1 &\stackrel{f}{\to}& X_2 } \;\;\; \simeq \;\;\; \array{ (b \circ f)^* A &\to& &\to& A \\ \downarrow && && \downarrow \\ B &\stackrel{b}{\to}& X_1 &\stackrel{f}{\to}& X_2 }

are isomorphic to the direct pullback along the composite on the right.

Related concepts

• strong functor

• cartesian closed category, locally cartesian closed category

• cartesian closed functor, locally cartesian closed functor

• cartesian closed model category, locally cartesian closed model category

• cartesian closed (∞,1)-category locally cartesian closed (∞,1)-category

References

For instance section A1.5 of

• Peter Johnstone, Sketches of an Elephant