With braiding
With duals for objects
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
With duals for morphisms
monoidal dagger-category?
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
A locally cartesian closed category is a category whose slice categories are all cartesian closed.
If a locally cartesian closed category has a terminal object, then is itself cartesian closed and in fact has all finite limits (because, cartesian products in are pullbacks in ); often this requirement is included in the definition.
Equivalently, a locally cartesian closed category is a category with pullbacks (and a terminal object, if required) such that each base change functor has a right adjoint , 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.
We show how the dependent product and the internal hom in the slice categories may be used to express each other.
Let be a category with pullbacks that has all dependent products , equivalently: such that every morphism in induces an base change adjoint triple
Then the internal hom in any slice exists and is given by
By the discussion at overcategory β limits and colimits, the product in the slice of two objects and is given by the pullback in , regarded again as a morphism over . More formally this means that the product with is given by the composite
of the pullback along with the dependent sum along . 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:
In a slice category of Sets, whose objects are -indexed sets, the inner hom is explicitly given by the indexed set of function sets between preimages:
And conversely:
If for a category every slice category is a cartesian closed category, then for every morphism in the dependent product exists and is given on an object by the pullback
in , where the bottom morphism is the adjunct of
It is sufficient to check the -adjunction hom set-natural isomorphism
natural in .
Since the hom functor preserves limits and hence pullbacks, the expression on the left is exhibited as the pullback
in Set. Using the -adjunction this is equivalently
This pullback now manifestly computes .
If is locally cartesian closed (i.e., if every slice is cartesian closed), then every slice is also locally cartesian closed.
The slice of a slice is a slice, i.e., for every there is an equivalence
whence the statement immediately follows.
If is locally cartesian closed (and has a terminal object), then the pullback functor preserves both finite products and exponentials up to isomorphism.
Clearly , being right adjoint to the forgetful functor , preserves limits, hence it preserves finite products in particular.
Let be any morphism. From the pullback diagram
we conclude , seen as an object over via . Thus arrows in the slice of the form
are in natural bijection with arrows in of the form
which in turn are in natural bijection with arrows in the slice of the form
(where is obtained by currying in ). This proves that preserves exponentials.
For any in , the base change preserves exponentials. In other words, the dependent sum functor and the dependent product functor satisfy Frobenius reciprocity.
This is by combining proposition and proposition , and recalling that the pullback functor
is identified with the pullback functor .
This state of affairs may be summarized in terms of the notion of hyperdoctrine:
If is a category with finite limits, then it is locally cartesian closed precisely if regarded as an -indexed category (by forming slice categories) it is a hyperdoctrine.
For a proof of the statement in this form, see for instance (Freyd).
We formulate some of the above considerations in the syntax of dependent type theory.
Let
be two display maps. Then the category theoretic identification
from prop. is the categorical semantics of the dependent type theory syntax
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 ) = ( collection of sections of the pullback of to )
By definition, the display map on the right is expressed as the dependent type
the pullback is expressed by substitution
and next the dependent product by
Now on the right , formally because is equivalently the projection out of expressed as the direct sum
Inserting this in the above expression makes it definitionally equal to
This is now a dependent product over a type that does not actually depend on the context , and hence by definition this is the dependent function type
which expresses the internal hom in the slice over .
The internal logic of locally cartesian closed categories is an extensional form of dependent type theory. In particular, the dependent product represents an extensional dependent product type in the internal logic.
There are categories which are cartesian closed and not locally cartesian closed, but in which for some the base change functor has a right adjoint. This includes , , and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for to be a fibration, while in it is sufficient for to be a fibration or an opfibration.
Every sheaf topos is locally cartesian closed.
By Giraud's theorem, in a sheaf topos pullbacks preserve colimits. With the adjoint functor theorem this implies that for every morphism , the pullback functor has a right adjoint . By prop. this yields the local cartesian closure.
More generally, every quasitopos is locally cartesian closed.
cartesian closed model category, locally cartesian closed model category
cartesian closed (β,1)-category, locally cartesian closed (β,1)-category
A standard textbook account is around corollary A1.5.3 in
Another textbook account, that also includes the set-theoretic intuition:
The relation between local cartesian closure and base change/hyperdoctrine structure is sometimes attributed to
A discussion of dependent type theory as the internal language of locally cartesian closed categories is in
exposition:
See also:
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.
Last revised on October 31, 2024 at 16:50:58. See the history of this page for a list of all contributions to it.