This page discusses the general concept of mapping spaces and internal homs. For mapping spaces in topology, see at compact-open topology.
hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
For a category and two objects, the internal hom from to is, if it exists, another object of which behaves like the βobject of morphismsβ from to . In other words it is, if it exists, an internal version of the ordinary hom set or more generally hom object of a locally small category or -enriched category.
One way to make this precise starts by mimicking a property of the function set of functions between two sets and : this set is characterized by the fact that for any other set , the functions are in natural bijection with the functions out of the cartesian product of with . That is: for each set , the functor has a right adjoint, given by the construction .
One can verbalize this thus: taking the cartesian product with the set is left-adjoint to taking the set of all functions with domain .
This, then, is, generally, the definition of internal hom in any cartesian monoidal category or in fact in any monoidal category : the right adjoint to the given tensor product functor for all objects . It may or may not exist. If it exists, one says that is a closed monoidal category. Explicity, the condition is that there is an isomorphism(bijection)
which is natural in all three variables. (The leftward map here is often called currying, especially in a closed monoidal category (and more especially for the -calculus).)
In particular this implies that in a closed monoidal category the external hom is re-obtained from the internal hom as its set of generalized elements out of the tensor unit in that
using that by definition of the tensor unit.
Here βclosedβ in βclosed monoidal categoryβ is in the sense that forming βhom-setsβ does not lead βout of the categoryβ. In fact the internal hom of a cartesian monoidal category is indeed the hom as seen in the internal logic of that category (the function type).
More generally, one can consider objects that satisfy some basic universal properties that an internal hom should satisfy even in the absence of a monoidal structure. If such objects exist one speaks therefore just of a closed category. Every closed category may be seen as a category enriched over itself. Accordingly, an internal hom is after all a special case of a hom-object, for the special case of this enrichment over itself.
(internal hom)
Let be a symmetric monoidal category. An internal hom in is a functor
such that for every object we have a pair of adjoint functors
If this exists, is called a closed monoidal category.
If the monoidal category in Def. is not symmetric, there is instead a concept of left- and right-internal hom.
Let be a symmetric closed monoidal category (Def. ).
If is specifically a locally cartesian closed category, then in terms of the type theory internal language of the evaluation map is the categorical semantics of the dependent type which in type theory syntax is
with function application on the right.
Let be a symmetric closed monoidal category (Def. )
For three objects, the composition morphism
is the -adjunct of the following composite of two evaluation maps, def. :
The internal homs in a symmetric closed monoidal category (Def. ) happen to share all the key abstract properties of ordinary (βexternalβ) hom-functors, even though this is not completely manifest from Def. :
Let be a symmetric monoidal category such that for each object the functor has a right adjoint . Then this is already equivalent to Def. , in that there is a unique functor out of the product category of with its opposite category
such that for each it coincides with the internal hom as a functor in the second variable, and such that there is a natural isomorphism
which is natural not only in and , but also in .
We have a natural isomorphism for each fixed , and hence in particular for fixed and fixed . With this the statement follows directly by this prop. at adjoint functor.
In fact the 3-variable adjunction from Prop. even holds internally:
(internal tensor/hom-adjunction)
In a closed monoidal category (def. ) there are natural isomorphisms
whose image under are the defining natural bijections of Prop. .
Let be any object. By applying the natural bijections from Prop. , there are composite natural bijections
Since this holds for all , the fully faithfulness of the Yoneda embedding says that there is an isomorphism . Moreover, by taking in the above and using the left unitor isomorphisms and we get a commuting diagram
Also the key respect of hom-functors for limits is inherited by internal hom-functors:
(internal hom-functor preserves limits)
Let be a symmetric closed monoidal category with internal hom-bifunctor (Prop. ). Then this bifunctor preserves limits in the second variable, and sends colimits in the first variable to limits:
and
For any object, is a right adjoint by definition, and hence preserves limits by adjoints preserve (co-)limits.
For the other case, let be a diagram in , and let be any object. Then there are isomorphisms
which are natural in , where we used that the ordinary hom-functor respects (co)limits as shown (see at hom-functor preserves limits), and that the left adjoint preserves colimits (see at adjoints preserve (co-)limits).
Hence by the fully faithfulness of the Yoneda embedding, there is an isomorphism
The internal hom is the categorical semantics of what in type theory are function types
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
function type | internal hom | |
type formation | ||
term introduction | ||
term elimination | ||
computation rule |
For each object the (internal hom tensor product)-adjunction induces a monad . In computer science this monad (in computer science) is called the state monad.
In topology the stabilization/suspension spectrum of mapping spaces between suitable CW-complexes happens to decompose as a direct sum of spectra in a useful way, related to the expression of the Goodwillie derivatives of the functor .
For more on this see at stable splitting of mapping spaces.
In the category Set of sets, regarded as a cartesian monoidal category, the internal hom is given by function sets. This exists, by the discussion there, as soon as the foundational axioms are strong enough, for instance as soon as there are power objects, which is the special case of a function set into the 2-element set.
In the category sSet of simplicial sets, the internal hom between two simplicial sets is given by the formula
where is the simplicial n-simplex. This is also called the function complex between and .
Since is the category of presheaves over the simplex category, this is a special case of internal homs in sheaf toposes, discussed below.
Let be a site. Let be the sheaf topos over or in fact the (β,1)-sheaf (β,1)-topos. We discuss the internal hom of this regard as a cartesian monoidal category/cartesian monoidal (β,1)-category.
The sheaf topos is a cartesian closed category / cartesian closed (β,1)-category. In fact it is a locally cartesian closed category / locally cartesian closed (β,1)-category.
Hence the internal hom exist.
For two objects, the internal hom-object
is the sheaf/(β,1)-sheaf given by the assignment
for all objects which on the right we regard under the Yoneda embedding/β-Yoneda embedding .
Here
is the cartesian product of with
is the hom set-functor / hom space-(β,1)-functor of .
See also at closed monoidal structure on presheaves.
By the Yoneda lemma/(β,1)-Yoneda lemma we have natural equivalences
and by the defining adjunction this is naturally equivalent to
In the (homotopy-)type theory syntax of the internal language of the internal hom is the categorical semantics of the function type
For , the evaluation map, def. ,
is the morphism of sheaves which over each sends a morphism of sheaves (which is the first component by prop. ) and an to
See (MacLane-Moerdijk, p. 46).
For three objects of , the canonical composition morphism, def. ,
is given by the morphism of presheaves/(β,1)-presheaves whose component over is the morphism of sets/β-groupoids
which sends a pair to the composite
where is the diagonal morphism on .
By definition the morphism is the adjunct of the double evaluation map
Since the cartesian product of two sheaves is computed objectwise
it follows that over each this double evaluation map is the morphism of sets/-groupoids
Intuitively this says that the composite of a -parameterized family of maps with a -parameterized family of maps is the -family given by the parameter-wise composite .
The internal automorphism group/automorphism β-group of an object is the subobject
of the internal hom which is maximal subject to the property that the composition of prop. becomes invertible.
The (homotopy-)type theory syntax for this is given by the type of equivalences in homotopy type theory
Let be a locally cartesian closed category. This means that for each object the slice category is a cartesian closed category. The product in the slice is given by the fiber product over computed in . Fairly detailed discussion of constructions of the internal hom in such slices is at locally cartesian closed category β cartesian closure in terms of base change and dependent product.
We record some further properties
For a locally cartesian closed category and any morphism in , the inverse image of the corresponding base change adjunction
is a cartesian closed functor.
This is discussed in more detail at cartesian closed functor β Examples.
So for we have isomorphisms
between the image of the internal hom under and the internal hom of the images of and separately.
For a locally cartesian closed category, any morphism, and two objects in the slice over , there is a natural morphism (not in general an isomorphism)
Here are two ways to get this morphism:
For any object we have a canonical morphism of hom sets
where the first and the last steps use adjunction properties, where the morphism in the middle is the component of the dependent sum functor, and where βFrob.Rec.β is Frobenius reciprocity.
Since this is natural in , the Yoneda lemma implies the claimed morphism.
There is the composite morphism
of the adjunction (co)units and the evaluation map of the internal hom. Its hom-adjunct is
using prop. on the right. The hom-adjunct of that in turn is
and by symmetry the morphism that we are after:
If is the terminal object (for simplicity), then the morphism of prop. can be understood as follows: a global element of the dependent product is given by a commuting diagram in of the form
The map in prop. picks out the top horizontal morphism in this diagram.
Consider the site SmthMfd of smooth manifolds (and the open cover coverage) or equivalently over the dense subsite CartSp of Cartesian spaces and smooth functions between these.
The sheaf topos/(β,1)-sheaf (β,1)-topos is that of smooth spaces/smooth β-groupoids. So the discussion of internal homs here is a special case of the above discussion In a sheaf topos.
For two smooth manifolds, the internal hom is the mapping space between them regarded as a diffeological space.
See at manifold structure of mapping spaces for when this internal hom is representable again by a smooth manifold.
For the internal automorphism group, example , of is the diffeomorphism group of , regarded as a diffeological group
The category of super vector spaces is the category of -graded vector spaces. Thus, its objects are pairs of vector spaces , with called the even part and the odd part. The morphisms in are likewise pairs of linear maps, i.e. we define to be , as usual for any sort of graded object. With this definition of the category , we capture the concepts of superalgebra and so on in succinct categorical terms.
Because the morphisms in send even things to even things and odd things to odd things, they are sometimes called even linear maps, and one may write
Note that is enriched over , i.e. these hom-sets are vector spaces.
Occasionally, however, one does need to refer to the odd linear maps, which send even things to odd things and odd things to even things. That is, an odd linear map is a pair of linear maps and . The internal-hom in allows us to capture these as well: it is the following super vector space:
With this definition, becomes a closed monoidal category.
We can equivalently regard a super vector spaces as being the direct sum vector space equipped with this direct sum decomposition. If we view the internal-hom in this way as well, then we have
In other words, any linear map between these βsummedβ super vector spaces decomposes uniquely as the sum of an even linear map and an odd one.
A similar thing happens in the category of Banach spaces and short linear operators. The external hom consists of only the short linear maps (those bounded by ):
This definition of morphism recovers the most specific notion of isomorphism of Banach spaces, as well as defining the product and coproduct as the direct sum completed with or respectively.
But the internal hom is the Banach space of all bounded linear maps:
This is a Banach space and makes into a closed category.
See any reference on closed categories and closed monoidal categories.
Also for instance:
Last revised on October 2, 2024 at 22:29:07. See the history of this page for a list of all contributions to it.