nLab internal hom

Contents

This page discusses the general concept of mapping spaces and internal homs. For mapping spaces in topology, see at compact-open topology.

Contents

1. Idea

For ๐’ž\mathcal{C} a category and X,Yโˆˆ๐’žX, Y \in \mathcal{C} two objects, the internal hom [X,Y]โˆˆ๐’ž[X,Y] \in \mathcal{C} from XX to YY is, if it exists, another object of ๐’ž\mathcal{C} which behaves like the โ€œobject of morphismsโ€ from XX to YY. In other words it is, if it exists, an internal version of the ordinary hom set ๐’ž(X,Y)โˆˆSet\mathcal{C}(X, Y) \in Set or more generally hom object ๐’ž(X,Y)โˆˆ๐’ฑ\mathcal{C}(X, Y) \in \mathcal{V} of a locally small category or ๐’ฑ\mathcal{V}-enriched category.

One way to make this precise starts by mimicking a property of the function set [X,Y]={f:Xโ†’Y}[X,Y] = \{f : X \to Y\} of functions between two sets XX and YY: this set is characterized by the fact that for any other set SS, the functions Sโ†’[X,Y]S \to [X,Y] are in natural bijection with the functions Sร—Xโ†’YS \times X \to Y out of the cartesian product of SS with XX. That is: for each set XX, the functor (โˆ’)ร—X(-) \times X has a right adjoint, given by the construction [X,โˆ’][X,-].

One can verbalize this thus: taking the cartesian product with the set XX is left-adjoint to taking the set of all functions with domain XX.

This, then, is, generally, the definition of internal hom in any cartesian monoidal category or in fact in any monoidal category (๐’ž,โŠ—)(\mathcal{C}, \otimes): the right adjoint [X,โˆ’][X,-] to the given tensor product functor (โˆ’)โŠ—X(-)\otimes X for all objects XX. It may or may not exist. If it exists, one says that (๐’ž,โŠ—)(\mathcal{C}, \otimes) is a closed monoidal category. Explicity, the condition is that there is an isomorphism(bijection)

๐’ž(A,[X,Z])โ†’โ‰ƒ๐’ž(AโŠ—X,Z) \mathcal{C}(A, [X,Z]) \stackrel{\simeq}{\to} \mathcal{C}(A \otimes X, Z)

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 ฮป\lambda-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 Iโˆˆ๐’žI \in \mathcal{C} in that

Iโ†’[X,Y]Xโ†’Y \frac{I \to [X,Y]}{X \to Y}

using that IโŠ—Xโ‰ƒXI \otimes X \simeq X 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.

2. Definition

Definition 2.1. (internal hom)

Let (๐’ž,โŠ—)(\mathcal{C}, \otimes) be a symmetric monoidal category. An internal hom in ๐’ž\mathcal{C} is a functor

[โˆ’,โˆ’]:๐’ž opร—๐’žโ†’๐’ž [-,-] : \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{C}

such that for every object Xโˆˆ๐’žX \in \mathcal{C} we have a pair of adjoint functors

((โˆ’)โŠ—XโŠฃ[X,โˆ’]):๐’žโ†’๐’ž. ((-) \otimes X \dashv [X, -]) : \mathcal{C} \to \mathcal{C} \,.

If this exists, (๐’ž,โŠ—)(\mathcal{C}, \otimes) is called a closed monoidal category.

Remark 2.2. If the monoidal category ๐’ž\mathcal{C} in Def. 2.1 is not symmetric, there is instead a concept of left- and right-internal hom.

Evaluation map

Let (๐’ž,โŠ—)(\mathcal{C}, \otimes) be a symmetric closed monoidal category (Def. 2.1).

Definition 2.3. For X,Yโˆˆ๐’žX,Y \in \mathcal{C} two objects, the evaluation map

eval X,Y:[X,Y]โŠ—Xโ†’Y eval_{X,Y} : [X,Y] \otimes X \to Y

is the ((โˆ’)โŠ—XโŠฃ[X,โˆ’])((-)\otimes X \dashv [X,-])-adjunct of the identity id [X,Y]:[X,Y]โ†’[X,Y]id_{[X,Y]} : [X,Y] \to [X,Y].

Remark 2.4. If ๐’ž\mathcal{C} is specifically a locally cartesian closed category, then in terms of the type theory internal language of ๐’ž\mathcal{C} the evaluation map is the categorical semantics of the dependent type which in type theory syntax is

f:Xโ†’Y,x:XโŠขf(x):Y, f \colon X \to Y,\; x \colon X \;\vdash\; f(x) \colon Y \,,

with function application on the right.

Composition map

Let (๐’ž,ร—)(\mathcal{C}, \times) be a symmetric closed monoidal category (Def. 2.1)

Definition 2.5. For X,Y,Zโˆˆ๐’žX, Y, Z \in \mathcal{C} three objects, the composition morphism

โˆ˜ X,Y,Z:[Y,Z]ร—[X,Y]โ†’[X,Z] \circ_{X,Y,Z} : [Y, Z] \times [X, Y] \to [X, Z]

is the ((โˆ’)ร—XโŠฃ[X,โˆ’])((-)\times X \dashv [X,-])-adjunct of the following composite of two evaluation maps, def. 2.3:

[Y,Z]ร—([X,Y]ร—X)โ†’(id [Y,Z],eval X,Y)[Y,Z]ร—Yโ†’eval Y,ZZ. [Y, Z] \times ([X , Y] \times X) \stackrel{(id_{[Y,Z]}, eval_{X,Y})}{\to} [Y,Z] \times Y \stackrel{eval_{Y,Z}}{\to} Z \,.

3. Properties

Basic properties

The internal homs in a symmetric closed monoidal category (Def. 2.1) happen to share all the key abstract properties of ordinary (โ€œexternalโ€) hom-functors, even though this is not completely manifest from Def. 2.1:

Proposition 3.1. (internal hom bifunctor)

Let ๐’ž\mathcal{C} be a symmetric monoidal category such that for each object Xโˆˆ๐’žX \in \mathcal{C} the functor XโŠ—(โˆ’)X \otimes (-) has a right adjoint [X,โˆ’][X,-]. Then this is already equivalent to Def. 2.1, in that there is a unique functor out of the product category of ๐’ž\mathcal{C} with its opposite category

[โˆ’,โˆ’]:๐’ž opร—๐’žโŸถ๐’ž [-,-] \;\colon\; \mathcal{C}^{op} \times \mathcal{C} \longrightarrow \mathcal{C}

such that for each Xโˆˆ๐’žX \in \mathcal{C} it coincides with the internal hom [X,โˆ’][X,-] as a functor in the second variable, and such that there is a natural isomorphism

Hom(X,[Y,Z])โ‰ƒHom(XโŠ—Y,Z) Hom(X, [Y,Z]) \;\simeq\; Hom(X \otimes Y, Z)

which is natural not only in XX and ZZ, but also in YY.

Proof. We have a natural isomorphism for each fixed YY, and hence in particular for fixed YY and fixed ZZ. With this the statement follows directly by this prop. at adjoint functor.ย ย โ–ฎ

In fact the 3-variable adjunction from Prop. 3.1 even holds internally:

Proposition 3.2. (internal tensor/hom-adjunction)

In a closed monoidal category (def. 2.1) there are natural isomorphisms

[XโŠ—Y,Z]โ‰ƒ[X,[Y,Z]] [X \otimes Y, Z] \;\simeq\; [X, [Y,Z]]

whose image under Hom ๐’ž(1,โˆ’)Hom_{\mathcal{C}}(1,-) are the defining natural bijections of Prop. 3.1.

Proof. Let Aโˆˆ๐’žA \in \mathcal{C} be any object. By applying the natural bijections from Prop. 3.1, there are composite natural bijections

Hom ๐’ž(A,[XโŠ—Y,Z]) โ‰ƒHom ๐’ž(AโŠ—(XโŠ—Y),Z) โ‰ƒHom ๐’ž((AโŠ—X)โŠ—Y,Z) โ‰ƒHom ๐’ž(AโŠ—X,[Y,Z]) โ‰ƒHom ๐’ž(A,[X,[Y,Z]]) \begin{aligned} Hom_{\mathcal{C}}(A , [X \otimes Y, Z]) & \simeq Hom_{\mathcal{C}}(A \otimes (X \otimes Y), Z) \\ & \simeq Hom_{\mathcal{C}}((A \otimes X)\otimes Y, Z) \\ & \simeq Hom_{\mathcal{C}}(A \otimes X, [Y,Z]) \\ & \simeq Hom_{\mathcal{C}}(A, [X, [Y,Z]]) \end{aligned}

Since this holds for all AA, the fully faithfulness of the Yoneda embedding says that there is an isomorphism [XโŠ—Y,Z]โ‰ƒ[X,[Y,Z]][ X\otimes Y, Z ] \simeq [X, [Y,Z]]. Moreover, by taking A=1A = 1 in the above and using the left unitor isomorphisms AโŠ—(XโŠ—Y)โ‰ƒXโŠ—YA \otimes (X \otimes Y) \simeq X \otimes Y and AโŠ—Xโ‰ƒXA\otimes X \simeq X we get a commuting diagram

Hom ๐’ž(1,[XโŠ—Y,Z]) โŸถโ‰ƒ Hom ๐’ž(1,[X,[Y,Z]]) โ‰ƒโ†“ โ†“ โ‰ƒ Hom ๐’ž(XโŠ—Y,Z) โŸถโ‰ƒ Hom ๐’ž(X,[Y,Z]). \array{ Hom_{\mathcal{C}}(1, [X\otimes Y, Z ]) &\overset{\simeq}{\longrightarrow}& Hom_{\mathcal{C}}(1, [X, [Y,Z]]) \\ {}^{\mathllap{\simeq}}\downarrow && \downarrow^{\mathrlap{\simeq}} \\ Hom_{\mathcal{C}}(X \otimes Y, Z) &\overset{\simeq}{\longrightarrow}& Hom_{\mathcal{C}}(X, [Y,Z]) } \,.

ย ย โ–ฎ

Also the key respect of hom-functors for limits is inherited by internal hom-functors:

Proposition 3.3. (internal hom-functor preserves limits)

Let ๐’ž\mathcal{C} be a symmetric closed monoidal category with internal hom-bifunctor [โˆ’,โˆ’][-,-] (Prop. 3.1). Then this bifunctor preserves limits in the second variable, and sends colimits in the first variable to limits:

[X,limโŸตjโˆˆ๐’ฅY(j)]โ‰ƒlimโŸตjโˆˆ๐’ฅ[X,Y(j)] [X, \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} Y(j)] \;\simeq\; \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} [X, Y(j)]

and

[limโŸถjโˆˆ๐’ฅY(j),X]โ‰ƒlimโŸตjโˆˆ๐’ฅ[Y(j),X] [\underset{\underset{j \in \mathcal{J}}{\longrightarrow}}{\lim} Y(j),X] \;\simeq\; \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} [Y(j),X]

Proof. For Xโˆˆ๐’žX \in \mathcal{C} any object, [X,โˆ’][X,-] is a right adjoint by definition, and hence preserves limits by adjoints preserve (co-)limits.

For the other case, let Y:โ„’โ†’๐’žY \;\colon\; \mathcal{L} \to \mathcal{C} be a diagram in ๐’ž\mathcal{C}, and let Cโˆˆ๐’žC \in \mathcal{C} be any object. Then there are isomorphisms

Hom ๐’ž(C,[limโŸถjโˆˆ๐’ฅY(j),X]) โ‰ƒHom ๐’ž(CโŠ—limโŸถjโˆˆ๐’ฅY(j),X) โ‰ƒHom ๐’ž(limโŸถjโˆˆ๐’ฅ(CโŠ—Y(j)),X) โ‰ƒlimโŸตjโˆˆ๐’ฅHom ๐’ž((CโŠ—Y(j)),X) โ‰ƒlimโŸตjโˆˆ๐’ฅHom ๐’ž(C,[Y(j),X]) โ‰ƒHom ๐’ž(C,limโŸตjโˆˆ๐’ฅ[Y(j),X]) \begin{aligned} Hom_{\mathcal{C}}(C, [ \underset{\underset{j \in \mathcal{J}}{\longrightarrow}}{\lim} Y(j), X ] ) & \simeq Hom_{\mathcal{C}}( C \otimes \underset{\underset{j \in \mathcal{J}}{\longrightarrow}}{\lim} Y(j), X ) \\ & \simeq Hom_{\mathcal{C}}( \underset{\underset{j \in \mathcal{J}}{\longrightarrow}}{\lim} (C \otimes Y(j)), X ) \\ & \simeq \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} Hom_{\mathcal{C}}( (C \otimes Y(j)), X ) \\ & \simeq \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} Hom_{\mathcal{C}}( C, [Y(j), X] ) \\ & \simeq Hom_{\mathcal{C}}( C, \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} [Y(j), X] ) \end{aligned}

which are natural in Cโˆˆ๐’žC \in \mathcal{C}, where we used that the ordinary hom-functor respects (co)limits as shown (see at hom-functor preserves limits), and that the left adjoint CโŠ—(โˆ’)C \otimes (-) preserves colimits (see at adjoints preserve (co-)limits).

Hence by the fully faithfulness of the Yoneda embedding, there is an isomorphism

[limโŸถjโˆˆ๐’ฅY(j),X]โŸถโ‰ƒlimโŸตjโˆˆ๐’ฅ[Y(j),X]. \left[ \underset{\underset{j \in \mathcal{J}}{\longrightarrow}}{\lim} Y(j), X \right] \overset{\simeq}{\longrightarrow} \underset{\underset{j \in \mathcal{J}}{\longleftarrow}}{\lim} [Y(j), X] \,.

ย ย โ–ฎ

Relation to function types

The internal hom is the categorical semantics of what in type theory are function types

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
function typeinternal hom
type formationโŠขX:TypeโŠขA:TypeโŠข(Xโ†’A):Type\frac{\vdash\: X \colon Type \;\;\;\;\; \vdash\; A\colon Type}{\vdash \; \left(X \to A\right) \colon Type}
term introductionx:XโŠขa(x):AโŠข(xโ†ฆa(x)):(Xโ†’A)\frac{x \colon X \;\vdash\; a(x) \colon A}{\vdash (x \mapsto a\left(x\right)) \colon \left(X \to A\right) }
term eliminationโŠขf:(Xโ†’A)โŠขx:XโŠขf(x):A\frac{\vdash\; f \colon \left(X \to A\right)\;\;\;\; \vdash \; x \colon X}{\;\;\;\vdash\; f(x) \colon A}
computation rule(yโ†ฆa(y))(x)=a(x)(y \mapsto a(y))(x) = a(x)

Induced monad (state monad)

For each object SS the (internal hom โŠฃ\dashv tensor product)-adjunction induces a monad [S,SโŠ—(โˆ’)][S, S \otimes (-)]. In computer science this monad (in computer science) is called the state monad.

Stable splitting

In topology the stabilization/suspension spectrum ฮฃ โˆžMaps(X,A)\Sigma^\infty Maps(X,A) of mapping spaces Maps(X,A)Maps(X,A) between suitable CW-complexes X,AX, A happens to decompose as a direct sum of spectra in a useful way, related to the expression of the Goodwillie derivatives of the functor Maps(X,โˆ’)Maps(X,-).

For more on this see at stable splitting of mapping spaces.

4. Examples

In sets

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 simplicial sets

In the category sSet of simplicial sets, the internal hom between two simplicial sets X,YX,Y is given by the formula

[X,Y] n=Hom sSet(Xร—ฮ”[n],Y), [X,Y]_n = Hom_{sSet}(X\times \Delta[n],Y) \,,

where ฮ”[n]\Delta[n] is the simplicial n-simplex. This [X,Y]โˆˆsSet[X,Y] \in sSet is also called the function complex between XX and YY.

Since sSetโ‰ƒPSh(ฮ”)sSet \simeq PSh(\Delta) is the category of presheaves over the simplex category, this is a special case of internal homs in sheaf toposes, discussed below.

In a sheaf topos or (โˆž,1)(\infty,1)-sheaf (โˆž,1)(\infty,1)-topos

Let CC be a site. Let H=Sh(C)\mathbf{H} = Sh(C) be the sheaf topos over CC 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.

Hence the internal hom exist.

Proposition 4.2. For X,YโˆˆHX, Y \in \mathbf{H} two objects, the internal hom-object

[X,Y]โˆˆH [X,Y] \in \mathbf{H}

is the sheaf/(โˆž,1)-sheaf given by the assignment

[X,Y]:Uโ†ฆH(Uร—X,Y), [X,Y] : U \mapsto \mathbf{H}(U \times X, Y) \,,

for all objects UโˆˆCU \in C which on the right we regard under the Yoneda embedding/โˆž-Yoneda embedding UโˆˆCโ†ชYonedaHU \in C \stackrel{Yoneda}{\hookrightarrow} \mathbf{H}.

Here

See also at closed monoidal structure on presheaves.

Proof. By the Yoneda lemma/(โˆž,1)-Yoneda lemma we have natural equivalences

[X,Y](U)โ‰ƒH(U,[X,Y]) [X,Y](U) \simeq \mathbf{H}(U , [X,Y])

and by the defining ((โˆ’)ร—XโŠข[X,โˆ’])((-)\times X \vdash [X,-])adjunction this is naturally equivalent to

โ‹ฏโ‰ƒH(Uร—X,Y). \cdots \simeq \mathbf{H}(U \times X, Y) \,.

ย ย โ–ฎ

Remark 4.3. In the (homotopy-)type theory syntax of the internal language of H\mathbf{H} the internal hom [X,Y]โˆˆH[X, Y] \in \mathbf{H} is the categorical semantics of the function type

โŠข(Xโ†’Y):Type. \vdash (X \to Y) : Type \,.

Proposition 4.4. For X,YโˆˆHX, Y \in \mathbf{H}, the evaluation map, def. 2.3,

eval X,Y:[X,Y]ร—Xโ†’Y eval_{X,Y} : [X,Y] \times X \to Y

is the morphism of sheaves which over each UโˆˆCU \in C sends a morphism of sheaves ฮธ:H(โˆ’,U)ร—X(โˆ’)โ†’Y(โˆ’)\theta : \mathbf{H}(-,U) \times X(-) \to Y(-) (which is the first component by prop. 4.2) and an xโˆˆH(U,X)x \in \mathbf{H}(U,X) to

eval X,Y(U):(ฮธ,x)โ†ฆฮธ U(id U,x)โˆˆY(U). eval_{X,Y}(U) : (\theta, x) \mapsto \theta_U(id_U, x) \in Y(U) \,.

See (MacLane-Moerdijk, p. 46).

Proposition 4.5. For X,Y,ZโˆˆHX, Y, Z \in \mathbf{H} three objects of H\mathbf{H}, the canonical composition morphism, def. 2.5,

โˆ˜ X,Y,Z:[Y,Z]ร—[X,Y]โ†’[X,Z] \circ_{X,Y,Z} : [Y, Z] \times [X, Y] \to [X, Z]

is given by the morphism of presheaves/(โˆž,1)-presheaves whose component over UโˆˆCU \in C is the morphism of sets/โˆž-groupoids

โˆ˜ X,Y,Z(U):H(Uร—X,Y)ร—H(Uร—Y,Z)โ†’H(Uร—X,Z) \circ_{X,Y,Z}(U) : \mathbf{H}(U \times X, Y) \times \mathbf{H}(U \times Y, Z) \to \mathbf{H}(U \times X, Z)

which sends a pair (f:Uร—Xโ†’Y,g:Uร—Yโ†’Z)(f : U \times X \to Y, g : U \times Y \to Z) to the composite

โˆ˜ X,Y,Z(U)(f,g)=Uร—Xโ†’(ฮ” U,id X)Uร—Uร—Xโ†’(id U,f)Uร—Yโ†’gZ, \circ_{X,Y,Z}(U)(f,g) = U \times X \stackrel{(\Delta_U, id_X)}{\to} U \times U \times X \stackrel{(id_U, f)}{\to} U \times Y \stackrel{g}{\to} Z \,,

where ฮ” U:Uโ†’Uร—U\Delta_U : U \to U \times U is the diagonal morphism on UU.

Proof. By definition 2.5 the morphism is the adjunct of the double evaluation map

[Y,Z]ร—[X,Y]ร—Xโ†’Z. [Y,Z] \times [X,Y] \times X \to Z \,.

Since the cartesian product of two sheaves A,BโˆˆHA, B \in \mathbf{H} is computed objectwise

Aร—B:Uโ†ฆA(U)ร—B(U) A \times B : U \mapsto A(U) \times B(U)

it follows that over each UโˆˆCU \in C this double evaluation map is the morphism of sets/โˆž\infty-groupoids

[Y,Z](U)ร—[X,Y](U)ร—X(U)โ†’Z(U) [Y,Z](U) \times [X,Y](U) \times X(U) \to Z(U)

hence by prop. 4.2

H(Uร—Y,Z)ร—H(Uร—X,Y)ร—H(U,X)โ†’H(U,Z), \mathbf{H}(U \times Y, Z) \times \mathbf{H}(U \times X, Y) \times \mathbf{H}(U,X) \to \mathbf{H}(U,Z) \,,

where now by prop. this is the external evaluation.ย ย โ–ฎ

Remark 4.6. Intuitively this says that the composite of a UU-parameterized family of maps {f(u):Xโ†’Y|uโˆˆU}\{f(u) : X \to Y| u \in U\} with a UU-parameterized family of maps g(u):Yโ†’Z|uโˆˆU{g(u) : Y \to Z| u \in U} is the UU-family given by the parameter-wise composite {g(u)โˆ˜f(u)|uโˆˆU}\{g(u)\circ f(u) | u \in U\}.

Example 4.7. The internal automorphism group/automorphism โˆž-group of an object XโˆˆHX \in \mathbf{H} is the subobject

Aut(X)โ†ช[X,X] \mathbf{Aut}(X) \hookrightarrow [X,X]

of the internal hom which is maximal subject to the property that the composition of prop. 4.5 becomes invertible.

The (homotopy-)type theory syntax for this is given by the type of equivalences in homotopy type theory

โŠข(Xโ†’โ‰ƒX):Type. \vdash (X \stackrel{\simeq}{\to} X) : Type \,.

In slice categories

Let H\mathbf{H} be a locally cartesian closed category. This means that for each object XโˆˆHX \in \mathbf{H} the slice category H /X\mathbf{H}_{/X} is a cartesian closed category. The product in the slice is given by the fiber product over XX computed in H\mathbf{H}. Fairly detailed discussion of constructions of the internal hom in such slices H /X\mathbf{H}_{/X} is at locally cartesian closed category โ€“ cartesian closure in terms of base change and dependent product.

We record some further properties

Proposition 4.8. For ๐’ž\mathcal{C} a locally cartesian closed category and f:Xโ†’Yf \colon X \to Y any morphism in ๐’ž\mathcal{C}, the inverse image f *f^* of the corresponding base change adjunction

๐’ž /Xโ†’โˆ fโ†f *โ†’โˆ‘ f๐’ž /Y \mathcal{C}_{/X} \stackrel{\overset{\sum_f}{\to}}{\stackrel{\overset{f^*}{\leftarrow}}{\underset{\prod_f}{\to}}} \mathcal{C}_{/Y}

is a cartesian closed functor.

This is discussed in more detail at cartesian closed functor โ€“ Examples.

So for A,Bโˆˆ๐’ž /YA,B \in \mathcal{C}_{/Y} we have isomorphisms

f *[A,B]โ†’โ‰ƒ[f *A,f *B] f^* \left[A,B\right] \stackrel{\simeq}{\to} \left[f^* A , f^* B\right]

between the image of the internal hom under f *f^* and the internal hom of the images of AA and BB separately.

Proposition 4.9. For H\mathbf{H} a locally cartesian closed category, f:Xโ†’Yf \colon X \to Y any morphism, and A,BโˆˆH /XA, B \in \mathbf{H}_{/X} two objects in the slice over XX, there is a natural morphism (not in general an isomorphism)

โˆ f[A,B]โ†’[โˆ‘ fA,โˆ‘ fB]. \prod_f \left[A,B \right] \to \left[ \sum_f A, \sum_f B\right] \,.

Here are two ways to get this morphism:

Proof/Construction 1. For any object UโˆˆH /YU \in \mathbf{H}_{/Y} we have a canonical morphism of hom sets

H /Y(U,โˆ f[A,B]) โ‰ƒH /X(f *U,[A,B]) โ‰ƒH /X(f *Uร—A,B) โ†’H /Y(โˆ‘ f(f *Uร—A),โˆ‘ fB) โ‰ƒFrob.Rec.H /Y(Uร—โˆ‘ fA,โˆ‘ fB) โ‰ƒH /Y(U,[โˆ‘ fA,โˆ‘ fB]) \begin{aligned} \mathbf{H}_{/Y}( U, \prod_f [A,B] ) & \simeq \mathbf{H}_{/X}( f^* U, [A,B] ) \\ & \simeq \mathbf{H}_{/X}(f^* U \times A, B) \\ & \stackrel{}{\to} \mathbf{H}_{/Y}( \sum_f( f^* U \times A ), \sum_f B ) \\ & \stackrel{Frob.Rec.}{\simeq} \mathbf{H}_{/Y}( U \times \sum_f A , \sum_f B ) \\ & \simeq \mathbf{H}_{/Y}(U, [\sum_f A , \sum_f B]) \end{aligned}

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 UU, the Yoneda lemma implies the claimed morphism.ย ย โ–ฎ

Proof/Construction 2. There is the composite morphism

(f *โˆ f[A,B])ร—Aโ†’counitร—id A[A,B]ร—Aโ†’evalBโ†’unitf *โˆ‘ fB \left(f^\ast \prod_f [A, B]\right) \times A \stackrel{counit \times id_A}{\to} [A, B] \times A \stackrel{eval}{\to} B \stackrel{unit}{\to} f^\ast \sum_f B

of the adjunction (co)units and the evaluation map of the internal hom. Its hom-adjunct is

Aโ†’[f *โˆ f[A,B],f *โˆ‘ fB]โ‰…f *[โˆ f[A,B],โˆ‘ fB], A \to [f^\ast \prod_f [A, B], f^\ast \sum_f B] \cong f^\ast [\prod_f [A, B], \sum_f B] \,,

using prop. 4.8 on the right. The hom-adjunct of that in turn is

โˆ‘ fAโ†’[โˆ f[A,B],โˆ‘ fB]\sum_f A \to [\prod_f [A, B], \sum_f B]

and by symmetry the morphism that we are after:

โˆ f[A,B]โ†’[โˆ‘ fA,โˆ‘ fB]. \prod_f [A, B] \to [\sum_f A, \sum_f B] \,.

ย ย โ–ฎ

Remark 4.10. If YY is the terminal object (for simplicity), then the morphism of prop. 4.9 can be understood as follows: a global element of the dependent product โˆ f[A,B]\prod_f [A,B] is given by a commuting diagram in H\mathbf{H} of the form

โˆ‘ fA โ†’ โˆ‘ fB โ†˜ โ†™ X. \array{ \sum_f A &&\to&& \sum_f B \\ & \searrow && \swarrow \\ && X } \,.

The map in prop. 4.9 picks out the top horizontal morphism in this diagram.

For smooth spaces and smooth โˆž\infty-groupoids

Consider the site C=C = 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 H=Sh(C)\mathbf{H} = Sh(C) 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.

Example 4.11. For X,YโˆˆSmthMfdโ†ชHX , Y \in SmthMfd \hookrightarrow \mathbf{H} two smooth manifolds, the internal hom [X,Y]โˆˆH[X,Y] \in \mathbf{H} 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.

Example 4.12. For XโˆˆSmthMfdโ†ชHX \in SmthMfd \hookrightarrow \mathbf{H} the internal automorphism group, example 4.7, of XX is the diffeomorphism group of XX, regarded as a diffeological group

Aut(X)=Diff(X). \mathbf{Aut}(X) = \mathbf{Diff}(X) \,.

For chain complexes

For super vector spaces

The category sVectsVect of super vector spaces is the category of โ„ค/2\mathbb{Z}/2-graded vector spaces. Thus, its objects are pairs of vector spaces (V +,V โˆ’)(V_+,V_-), with V +V_+ called the even part and V โˆ’V_- the odd part. The morphisms in sVectsVect are likewise pairs of linear maps, i.e. we define sVectsVect to be Vectร—Vect=Vect โ„ค/2Vect \times Vect = Vect^{\mathbb{Z}/2}, as usual for any sort of graded object. With this definition of the category sVectsVect, we capture the concepts of superalgebra and so on in succinct categorical terms.

Because the morphisms in sVectsVect send even things to even things and odd things to odd things, they are sometimes called even linear maps, and one may write

sVect(V,W)=EvenLin(V,W). sVect(V, W) = Even Lin(V,W).

Note that sVectsVect is enriched over VectVect, 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 Vโ†’WV\to W is a pair of linear maps V +โ†’W โˆ’V_+ \to W_- and V โˆ’โ†’W +V_-\to W_+. The internal-hom in sVectsVect allows us to capture these as well: it is the following super vector space:

[V,W] +=EvenLin(V,W)[V,W] โˆ’=OddLin(V,W). [V,W]_+ = Even Lin(V,W) \qquad [V,W]_- = Odd Lin(V,W).

With this definition, sVectsVect becomes a closed monoidal category.

We can equivalently regard a super vector spaces (V +,V โˆ’)(V_+,V_-) as being the direct sum vector space V +โŠ•V โˆ’V_+ \oplus V_- equipped with this direct sum decomposition. If we view the internal-hom [V,W][V,W] in this way as well, then we have

[V,W]=EvenLin(V,W)โŠ•OddLin(V,W)=Lin(V,W). [V, W] = Even Lin(V,W) \oplus Odd Lin(V,W) = Lin(V,W).

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.

For Banach spaces

A similar thing happens in the category BanBan of Banach spaces and short linear operators. The external hom consists of only the short linear maps (those bounded by 11):

Ban(V,W)={f:Lin(V,W)|โ€–fโ€–โ‰ค1}. Ban(V,W) = \{ f\colon Lin(V,W) \;|\; {\|f\|} \leq 1 \} .

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 p=โˆžp = \infty or p=1p = 1 respectively.

But the internal hom is the Banach space of all bounded linear maps:

[V,W]={f:Lin(V,W)|โ€–fโ€–<โˆž}. [V,W] = \{ f\colon Lin(V,W) \;|\; {\|f\|} \lt \infty \} .

This is a Banach space and makes BanBan into a closed category.

6. References

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.