nLab
locally cartesian closed category

Context

Category Theory

Monoidal categories

Contents

Definition

A locally cartesian closed category is a category CC whose slice categories C/xC/x are all cartesian closed.

If a locally cartesian closed category CC has a terminal object, then CC is itself cartesian closed and in fact has all finite limits (because, cartesian products in C/xC/x are pullbacks in CC); often this requirement is included in the definition.

Equivalently, a locally cartesian category CC is a category with pullbacks (and a terminal object, if required) such that each base change functor f *:C/y→C/xf^*: C/y \to C/x has a right adjoint Π f\Pi_f, called the dependent product. (This equivalence is discussed in detail below.)

In particular, such pullbacks preserve all colimits. Therefore, if a locally cartesian closed category has finite colimits, it is automatically a coherent category and in fact a Heyting category.

Properties

Cartesian closure in terms of base change and dependent product

We show how the dependent product and the internal hom in the slice categories may be used to express each other.

In category theory

Proposition

Let π’ž\mathcal{C} be a category with pullbacks that has all dependent products ∏ β€’\prod_\bullet, equivalently that every morphism f:Eβ†’Xf : E \to X in π’ž\mathcal{C} induces an adjoint triple

π’ž /Eβ†’βˆ f←f *β†’βˆ‘ fπ’ž /X. \mathcal{C}_{/E} \stackrel{\overset{\sum_f}{\to}}{\stackrel{\overset{f^*}{\leftarrow}}{\underset{\prod_f}{\to}}} \mathcal{C}_{/X} \,.

Then the internal hom in a slice π’ž /X\mathcal{C}_{/X} exists and is given by

[⟨Eβ†’fX⟩,βˆ’] π’ž /Xβ‰ƒβˆ f∘f *. [\langle E \stackrel{f}{\to} X\rangle \; ,\; -]_{\mathcal{C}_{/X}} \simeq \prod_f \circ f^* \,.
Proof

By the discusson at overcategory-Limits and colimits the product in the slice π’ž /X\mathcal{C}_{/X} of two objects ⟨E 1β†’f 1X⟩\langle E_1 \stackrel{f_1}{\to} X\rangle and ⟨E 1β†’f 2X⟩\langle E_1 \stackrel{f_2}{\to} X\rangle is given by the pullback f 1 *E 2=f 2 *E 1f_1^* E_2 = f_2^* E_1 in π’ž\mathcal{C}, regarded again as a morphism over XX. More formally this means that the product with ⟨Eβ†’fX⟩\langle E \stackrel{f}{\to} X\rangle is given by the composite

(βˆ’)Γ— π’ž /X⟨Eβ†’fX⟩:π’ž /Xβ†’f *π’ž /Eβ†’βˆ‘ fπ’ž /X (-) \times_{\mathcal{C}_{/X}} \langle E \stackrel{f}{\to} X\rangle \;\;\;:\;\;\; \mathcal{C}_{/X} \stackrel{f^*}{\to} \mathcal{C}_{/E} \stackrel{\sum_f}{\to} \mathcal{C}_{/X}

of the pullback along ff with the dependent sum along ff. By the above adjoint triple both these morphisms have right adjoints and so the composite of the right adjoints is the right adjoint of the composite, hence is the internal hom:

π’ž /Xβ†βˆ fπ’ž /E←f *π’ž /X:[⟨Eβ†’fX⟩,βˆ’] π’ž /X. \mathcal{C}_{/X} \stackrel{\prod_f}{\leftarrow} \mathcal{C}_{/E} \stackrel{f^* }{\leftarrow} \mathcal{C}_{/X} \;\;\;:\;\;\; [\langle E\stackrel{f}{\to} X \rangle, -]_{\mathcal{C}_{/X}} \,.
Example

In the slice category Set/XSet/X, the inner hom is explicitly given by

[⟨Eβ†’fX⟩,⟨Fβ†’gX⟩] Set/X={(x,h)∣x∈X,h:f βˆ’1(x)β†’g βˆ’1(x)}. [\langle E \stackrel{f}{\to} X \rangle, \langle F \stackrel{g}{\to} X \rangle]_{Set/X} = \{ (x,h) | x \in X, h : f^{-1}(x) \to g^{-1}(x) \}.
Proposition

If for a category π’ž\mathcal{C} every slice category is a cartesian closed category, then for every morphism f:Xβ†’Yf : X \to Y in π’ž\mathcal{C} the dependent product ∏ f\prod_f exists and is given on an object Eβ†’pXE \stackrel{p}{\to} X by the pullback

∏ f⟨Eβ†’pX⟩ β†’ [⟨Xβ†’fY⟩,⟨Eβ†’pXβ†’fY⟩] π’ž /Y ↓ ↓ Y β†’idΒ― [⟨Xβ†’fY⟩,⟨Xβ†’fY⟩] π’ž /Y \array{ \prod_f \langle E \stackrel{p}{\to} X\rangle &\to& [\langle X \stackrel{f}{\to}Y\rangle, \langle E \stackrel{p}{\to}X \stackrel{f}{\to} Y\rangle]_{\mathcal{C}_{/Y}} \\ \downarrow && \downarrow \\ Y &\stackrel{\bar id}{\to}& [\langle X \stackrel{f}{\to}Y \rangle,\langle X \stackrel{f}{\to}Y \rangle]_{\mathcal{C}_{/Y}} }

in π’ž /Y\mathcal{C}_{/Y}, where the bottom morphism is the adjunct of

YΓ— π’ž /Y⟨Xβ†’fYβŸ©β‰ƒβŸ¨Xβ†’fYβŸ©β†’id⟨Xβ†’fY⟩. Y \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to} Y\rangle \simeq \langle X \stackrel{f}{\to}Y\rangle \stackrel{id}{\to} \langle X \stackrel{f}{\to}Y\rangle \,.
Proof

It is sufficient to check the (f *⊣∏ f)(f^* \dashv \prod_f)-adjunction hom set-natural isomorphism

π’ž /Y(⟨Fβ†’Y⟩,∏ f⟨Eβ†’pX⟩)β‰ƒπ’ž /X(f *⟨Fβ†’Y⟩,⟨Eβ†’pX⟩), \mathcal{C}_{/Y}( \langle F \stackrel{}{\to} Y\rangle , \prod_f \langle E \stackrel{p}{\to} X\rangle) \simeq \mathcal{C}_{/X}(f^* \langle F \stackrel{}{\to} Y\rangle, \langle E \stackrel{p}{\to} X\rangle) \,,

natural in ⟨Fβ†’Y⟩\langle F \stackrel{}{\to}Y \rangle.

Since the hom functor π’ž /Y(⟨Fβ†’Y⟩,βˆ’)\mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, -) preserves limits and hence pullbacks, the expression on the left is exhibited as the pullback

π’ž /Y(⟨Fβ†’Y⟩,∏ f⟨Eβ†’pX⟩ β†’ π’ž /Y(⟨Fβ†’Y⟩,[⟨Xβ†’fY⟩,⟨Eβ†’pXβ†’fY⟩] π’ž /Y) ↓ ↓ * β†’ π’ž /Y(⟨Fβ†’Y⟩,[⟨Xβ†’fY⟩,⟨Xβ†’fY⟩] π’ž /Y) \array{ \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, \prod_f \langle E \stackrel{p}{\to} X\rangle &\to& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, [\langle X \stackrel{f}{\to}Y \rangle,\langle E \stackrel{p}{\to}X \stackrel{f}{\to} Y\rangle]_{\mathcal{C}_{/Y}}) \\ \downarrow && \downarrow \\ * &\stackrel{}{\to}& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle,[\langle X \stackrel{f}{\to}Y \rangle,\langle X \stackrel{f}{\to}Y \rangle]_{\mathcal{C}_{/Y}}) }

in Set. Using the ((βˆ’)Γ— π’ž /Y⟨Xβ†’fY⟩⊣[⟨Xβ†’fY⟩,βˆ’] π’ž /Y)((-) \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to}Y\rangle \dashv [\langle X \stackrel{f}{\to}Y\rangle, -]_{\mathcal{C}_{/Y}})-adjunction this is equivalently

π’ž /Y(⟨Fβ†’Y⟩,∏ f⟨Eβ†’pX⟩ β†’ π’ž /Y(⟨Fβ†’YβŸ©Γ— π’ž /Y⟨Xβ†’fY⟩,⟨Eβ†’pXβ†’fY⟩) ↓ ↓ * β†’ π’ž /Y(⟨Fβ†’YβŸ©Γ— π’ž /Y⟨Xβ†’fY⟩,⟨Xβ†’fY⟩). \array{ \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, \prod_f \langle E \stackrel{p}{\to} X\rangle &\to& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to}Y \rangle, \langle E \stackrel{p}{\to}X \stackrel{f}{\to} Y\rangle) \\ \downarrow && \downarrow \\ * &\stackrel{}{\to}& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle \times_{\mathcal{C}_{/Y} }\langle X \stackrel{f}{\to}Y \rangle , \langle X \stackrel{f}{\to}Y \rangle) } \,.

This pullback now manifestly computes π’ž /X(f *⟨Fβ†’Y⟩,⟨Eβ†’pX⟩)\mathcal{C}_{/X}(f^* \langle F \to Y\rangle, \langle E \stackrel{p}{\to} X\rangle).

Proposition

If CC is locally cartesian closed (i.e., if every slice C/XC/X is cartesian closed), then every slice C/XC/X is also locally cartesian closed.

Proof

The slice of a slice is a slice, i.e., for every f:X→Yf \colon X \to Y there is an equivalence

(C/Y)/(f:Xβ†’Y)≃C/X(C/Y)/(f \colon X \to Y) \simeq C/X

whence the statement immediately follows.

Proposition

If CC is locally cartesian closed (and has a terminal object), then the pullback functor XΓ—βˆ’:Cβ†’C/XX \times - \colon C \to C/X preserves both finite products and exponentials up to isomorphism.

Proof

Clearly XΓ—βˆ’:Cβ†’C/xX \times - \colon C \to C/x, being right adjoint to the forgetful functor βˆ‘ X:C/Xβ†’C\sum_X \colon C/X \to C, preserves limits, hence it preserves finite products in particular.

Let ϕ:A→X\phi \colon A \to X be any morphism. From the pullback diagram

AΓ—Z →ϕ×1 XΓ—Z Ο€ A↓ ↓ Ο€ X A β†’Ο• X\array{ A \times Z & \stackrel{\phi \times 1}{\to} & X \times Z \\ _\mathllap{\pi_A} \downarrow & & \downarrow _\mathrlap{\pi_X} \\ A & \underset{\phi}{\to} & X }

we conclude AΓ— X(XΓ—Z)β‰…AΓ—ZA \times_X (X \times Z) \cong A \times Z, seen as an object over XX via Ο•βˆ˜Ο€ A:AΓ—Zβ†’X\phi \circ \pi_A \colon A \times Z \to X. Thus arrows in the slice C/XC/X of the form

AΓ— X(XΓ—Z)β†’XΓ—YA \times_X (X \times Z) \to X \times Y

are in natural bijection with arrows in CC of the form

AΓ—Zβ†’βŸ¨Ο•βˆ˜Ο€ A,g⟩XΓ—YA \times Z \stackrel{\langle \phi \circ \pi_A, g\rangle}{\to} X \times Y

which in turn are in natural bijection with arrows in the slice C/XC/X of the form

Aβ†’βŸ¨Ο•,g˜⟩XΓ—Y ZA \stackrel{\langle \phi, \tilde{g} \rangle}{\to} X \times Y^Z

(where g˜:Aβ†’Y Z\tilde{g} \colon A \to Y^Z is obtained by currying g:AΓ—Zβ†’Yg \colon A \times Z \to Y in CC). This proves that XΓ—βˆ’:Cβ†’C/xX \times - \colon C \to C/x preserves exponentials.

Corollary

For any f:Xβ†’Yf \colon X \to Y in CC, the base change f *:C/Yβ†’C/Xf^\ast \colon C/Y \to C/X preserves exponentials. In other words, the dependent sum functor βˆ‘ f\sum_f and the dependent product functor ∏ f\prod_f satisfy Frobenius reciprocity.

Proof

This is by combining proposition 3 and proposition 4, and recalling that the pullback functor

C/Yβ†’(C/Y)/(f:Xβ†’Y)≃C/XC/Y \to (C/Y)/(f \colon X \to Y) \simeq C/X

is identified with the pullback functor f *:C/Y→C/Xf^\ast \colon C/Y \to C/X.

This state of affairs may be summarized in terms of the notion of hyperdoctrine:

Proposition

If CC is a category with finite limits, then it is locally cartesian closed precisely if regarded as an CC-indexed category (by forming slice categories) it is a hyperdoctrine.

For a proof of the statement in this form, see for instance (Freyd).

In type theory

We formulate some of the above considerations in the syntax of dependent type theory.

Proposition

Let

X A Ο•β†˜ ↙ c B \array{ X &&&& A \\ & {}_{\mathllap{\phi}}\searrow && \swarrow_{\mathrlap{c}} \\ && B }

be two display maps. Then the category theoretic identification

[X,A] B=∏ ϕϕ *⟨Aβ†’cX⟩ [X,A]_{B} = \prod_\phi \phi^* \langle A \stackrel{c}{\to} X\rangle

from prop. 1 is the categorical semantics of the dependent type theory syntax

b:B⊒X(b)β†’A(b):Type= defb:B⊒∏ x:X(b)A(Ο•(x)). b : B \vdash X(b) \to A(b) : Type \;\;\; =_{def} \;\;\; b : B \vdash \prod_{x : X(b)} A(\phi(x)) \,.
Remark

While equivalent under the relation between type theory and category theory, the latter expression almost verbatim expresses the evident idea that:

(collection of internal homs parameterized over BB) = ( collection of sections of the pullback of AA to XX )

Proof

By definition, the display map on the right is expressed as the dependent type

b:B⊒A(b):Type, b : B \vdash A(b) : Type \,,

the pullback f *⟨Aβ†’B⟩f^* \langle A \to B\rangle is expressed by substitution

x:X⊒A(Ο•(x)):Type x : X \vdash A(\phi(x)) : Type

and next the dependent product ∏ ϕϕ *⟨Aβ†’B⟩\prod_\phi \phi^* \langle A \to B\rangle by

b:B⊒∏ x:X(b)A(Ο•(x)):Type. b : B \vdash \prod_{x : X(b)} A(\phi(x)) : Type \,.

Now on the right Ο•(x)= defb\phi(x) =_{def} b, formally because Ο•\phi is equivalently the projection pr 1pr_1 out of XX expressed as the direct sum

(b,x):βˆ‘ b:BX(b)pr 1(b,x)= defb= defΟ•(x):B. \frac{(b,x) : \sum_{b : B} X(b)} { pr_1(b,x) =_{def} b =_{def} \phi(x) : B} \,.

Inserting this in the above expression makes it definitionally equal? to

b:B⊒∏ x:X(b)A(b):Type. b : B \vdash \prod_{x : X(b)} A(b) : Type \,.

This in now a dependent product over a type that does not actually depend on the context BB, and hence by definition this is the dependent function type

b:B⊒X(b)β†’A(b):Type. b : B \vdash X(b) \to A(b) : Type \,.

which expresses the internal hom in the slice over BB.

Internal logic

The internal logic of locally cartesian closed categories is an extensional form of dependent type theory. In particular, the dependent product Ξ  f\Pi_f represents an extensional dependent product type in the internal logic.

Almost local cartesian closure

There are categories which are cartesian closed and not locally cartesian closed, but in which for some ff the base change functor f *:C/y→C/xf^*: C/y \to C/x has a right adjoint. This includes CatCat, GpdGpd, and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for ff to be a fibration, while in CatCat it is sufficient for ff to be a fibration or an opfibration.

Examples

Proposition

Every sheaf topos is locally cartesian closed.

Proof

By Giraud's theorem, in a sheaf topos pullbacks preserve colimits. With the adjoint functor theorem this implies that for every morphism f:Xβ†’Yf : X \to Y, the pullback functor f *:π’ž /Yβ†’π’ž /Xf^* : \mathcal{C}_{/Y} \to \mathcal{C}_{/X} has a right adjoint ∏ f\prod_f. By prop. 1 this yields the local cartesian closure.

References

A standard textbook account is around corollary A1.5.3 in

The relation between local cartesian closure and base change/hyperdoctrine structure is sometimes attributed to

  • Peter Freyd, Aspects of topoi, Bull. Australian Math. Soc. 7 (1972), 1-76.

A discussion of dependent type theory as the internal language of locally cartesian closed categories is in

  • R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

Related literature includes

  • Marta Bunge, and Susan Niefield, Exponentiability and single universes J. Pure Appl. Algebra 148 (2000) 217–250.

  • FranΓ§ois ConduchΓ©, Au sujet de l’existence d’adjoints Γ  droite aux foncteurs β€œimage rΓ©ciproque” dans la catΓ©gorie des catΓ©gories (French) C. R. Acad. Sci. Paris SΓ©r. A-B 275 (1972), A891–A894.

  • J. Howie, Pullback functors and crossed complexes , Cahiers Topologie GΓ©om. DiffΓ©rentielle, 20 (1979) 281–296.

Revised on March 28, 2014 06:48:28 by Tim Porter (2.26.28.93)