Closed Monoidal Categories and the Internal Hom

If $R,R^{\mathrm{\prime }}:\mathcal{C}\to \mathcal{C}$ are two chosen right adjoints to $-\otimes X$, then they are two right adjoints to the same functor. By [L2] there is a unique natural isomorphism $R\Rightarrow R^{\mathrm{\prime }}$ compatible with the adjunction units and counits.

By [L1], a right internal hom in the variable $X$ is precisely such a right adjoint $R=[X,-]$. Therefore any two choices of $[X,-]$, equipped with their adjunction data, are related by the unique natural isomorphism compatible with those units and counits.

The same argument with the functor $X\otimes -$ proves the corresponding adjunction-compatible uniqueness for the left internal hom $⟨X,-⟩$.

So both internal-hom constructions, with their adjunction data fixed, are unique up to a unique compatible natural isomorphism.

For each $A,Y$, compose the bijection of [L1] with precomposition by ${\sigma }_A^{-1}:X\otimes A\to A\otimes X$. This gives a natural bijection $\mathcal{C}(X\otimes A,Y)\cong \mathcal{C}(A,[X,Y])$.

The bijection in step 1.1 says exactly that $[X,-]$ is also a right adjoint to the functor $X\otimes -$. Hence a left internal hom for $X$ exists and may be chosen to be $[X,-]$.

Any other chosen right adjoint to $X\otimes -$ is uniquely naturally isomorphic to $[X,-]$ by [L2]. Therefore the supplied symmetry identifies the left and right internal homs, and a genuine symmetric monoidal structure gives this conclusion for every $X$.

Since $\mathcal{C}$ is biclosed, the functor $-\otimes X$ has a right adjoint and is therefore a left adjoint by [L1].

Likewise $X\otimes -$ has a right adjoint and is a left adjoint.

Apply [L2] to step 1.1 to conclude that $-\otimes X$ preserves every colimit that exists in $\mathcal{C}$.

Apply [L2] to step 1.2 to conclude that $X\otimes -$ preserves every colimit that exists in $\mathcal{C}$.

Hence tensoring with a fixed object is cocontinuous in each variable.

Fix $X$. By [L1], the functor $[X,-]$ is a right adjoint, so [L2] implies that it preserves every limit that exists in $\mathcal{C}$.

Fix $Y$. For a morphism $u:X^{\mathrm{\prime }}\to X$, define $[u,Y]:[X,Y]\to [X^{\mathrm{\prime }},Y]$ to be the transpose of

Let $(i_j:X_j\to X)$ be a colimit cocone in $\mathcal{C}$, and fix an object $A$. By [L3], the functor $A\otimes -$ preserves this colimit, so maps $A\otimes X\to Y$ are naturally the same as compatible families of maps $A\otimes X_j\to Y$.

Apply the transposition bijection of [L1] to the maps in step 2.1. A map $A\otimes X\to Y$ is the same as a map $A\to [X,Y]$, and a compatible family $A\otimes X_j\to Y$ is the same as a compatible family $A\to [X_j,Y]$ with respect to the morphisms $[i_j,Y]$ from step 1.2. Therefore maps $A\to [X,Y]$ are naturally in bijection with cones from $A$ to the diagram $j\mapsto [X_j,Y]$, so $[X,Y]$ is a limit of that diagram.

Hence the contravariant functor $[-,Y]:{\mathcal{C}}^{\mathrm{o}\mathrm{p}}\to \mathcal{C}$ sends colimits in $\mathcal{C}$ to limits in $\mathcal{C}$, equivalently preserves limits in ${\mathcal{C}}^{\mathrm{o}\mathrm{p}}$. Combining this with step 1.1 proves the claim.

Consider the composite $([Y,Z]\otimes [X,Y])\otimes X\cong [Y,Z]\otimes ([X,Y]\otimes X)\stackrel{1\otimes {\mathrm{ev}}_{X,Y}}{\to }[Y,Z]\otimes Y\stackrel{{\mathrm{ev}}_{Y,Z}}{\to }Z$. Transposing it across the adjunction $-\otimes X⊣[X,-]$ gives a unique morphism ${\mathrm{comp}}_{X,Y,Z}:[Y,Z]\otimes [X,Y]\to [X,Z]$.

Transpose the left unitor ${\lambda }_X:\mathbf{1}\otimes X\to X$ across the same adjunction to obtain $u_X:\mathbf{1}\to [X,X]$.

To compare the two composites $[Z,W]\otimes [Y,Z]\otimes [X,Y]\rightrightarrows [X,W]$, tensor each with $X$ and postcompose with ${\mathrm{ev}}_{X,W}$. Both have the same transpose, namely the triple evaluation map $[Z,W]\otimes [Y,Z]\otimes [X,Y]\otimes X\to W$, so the transposition bijection of [L1] forces the two composites to be equal.

The left and right unit laws are proved the same way: after tensoring with $X$ and evaluating, both candidate composites have transpose ${\mathrm{ev}}_{X,Y}$. Hence the transposition bijection identifies them, so $u$ is a unit for $\mathrm{comp}$.

Therefore the internal hom carries a natural composition morphism and objectwise unit morphisms satisfying associativity and the unit laws.

The right unitor gives natural isomorphisms $A\otimes \mathbf{1}\cong A$. Applying the transposition bijection of [L1] with $X=\mathbf{1}$ therefore gives natural bijections $\mathcal{C}(A,Y)\cong \mathcal{C}(A\otimes \mathbf{1},Y)\cong \mathcal{C}(A,[\mathbf{1},Y])$. So the identity functor is also a right adjoint to $-\otimes \mathbf{1}$. Since $[\mathbf{1},-]$ is another right adjoint to the same functor, [L2] gives $[\mathbf{1},Y]\cong Y$ naturally in $Y$.

Apply the transposition bijection of [L1] with $A=\mathbf{1}$. Because $\mathbf{1}\otimes X\cong X$, this gives $\mathcal{C}(X,Y)\cong \mathcal{C}(\mathbf{1},[X,Y])$. Rewriting the bijection in the opposite direction yields the displayed form.

Thus the tensor unit recovers the external hom-set from the internal hom.

By [L2], $\mathbf{S}\mathbf{e}\mathbf{t}$ has finite products.

Let $C^B$ be the set of functions $B\to C$, and let $\mathrm{ev}:C^B\times B\to C$ send $(f,b)$ to $f(b)$. By [L3], every map $A\times B\to C$ corresponds naturally and bijectively to a map $A\to C^B$. This is exactly the universal property of an exponential object.

Step 1.1 gives the finite-product part of [L1], and step 1.2 gives the right adjoint to $-\times B$ for each $B$. Therefore $\mathbf{S}\mathbf{e}\mathbf{t}$ is cartesian closed.

By [L1], $\mathbf{C}\mathbf{a}\mathbf{t}$ has the finite products required in [L3]. By [L2], the functor category $[\mathcal{D},\mathcal{E}]$ is again a small category.

A functor $F:\mathcal{C}\times \mathcal{D}\to \mathcal{E}$ determines a functor $\tilde{F}:\mathcal{C}\to [\mathcal{D},\mathcal{E}]$ by $\tilde{F}(c)(d)=F(c,d)$ on objects and similarly on morphisms. Conversely, a functor $\mathrm{\Phi }:\mathcal{C}\to [\mathcal{D},\mathcal{E}]$ determines $\widehat{\mathrm{\Phi }}:\mathcal{C}\times \mathcal{D}\to \mathcal{E}$ by evaluation, $\widehat{\mathrm{\Phi }}(c,d)=\mathrm{\Phi }(c)(d)$. These assignments are inverse and natural in $\mathcal{C}$.

Step 1.2 is exactly the adjunction $\mathbf{C}\mathbf{a}\mathbf{t}(\mathcal{C}\times \mathcal{D},\mathcal{E})\cong \mathbf{C}\mathbf{a}\mathbf{t}(\mathcal{C},[\mathcal{D},\mathcal{E}])$. Thus $-\times \mathcal{D}$ has right adjoint $[\mathcal{D},-]$. With step 1.1, [L3] now gives that $\mathbf{C}\mathbf{a}\mathbf{t}$ is cartesian closed.

By [L4], binary products in $\widehat{\mathcal{C}}$ are computed pointwise, so $H\times P$ is the presheaf with $(H\times P)(c)=H(c)\times P(c)$. The assignment $c\mapsto \mathrm{Nat}(y(c)\times P,Q)$ with restriction by precomposition along $y(f)\times 1_P$ is therefore a presheaf $Q^P$.

Given $\alpha :H\to Q^P$, define $\tilde{\alpha }:H\times P\to Q$ by sending $(h,p)\in H(c)\times P(c)$ to the element of $Q(c)$ corresponding under [L2] to the natural transformation $y(c)\stackrel{h}{\to }H\stackrel{\alpha }{\to }{Q}^P$, evaluated at $p$. Conversely, given $\beta :H\times P\to Q$, use [L2] and the set-level currying of [L3] objectwise to define ${\widehat{\beta }}_c(h)\in \mathrm{Nat}(y(c)\times P,Q)$; naturality in $c$ is exactly the restriction rule from step 1.1.

The two constructions of step 2.1 are inverse because Yoneda identifies a natural transformation out of $y(c)$ with its value at $1_c$, and the set-level currying and uncurrying in [L3] are inverse. Hence $\widehat{\mathcal{C}}(H\times P,Q)\cong \widehat{\mathcal{C}}(H,Q^P)$ naturally in $H$.

Step 3.1 shows that $-\times P$ has right adjoint $(-{)}^P$, while [L4] gives the finite products. Therefore [L5] implies that $\widehat{\mathcal{C}}$ is cartesian closed.

By [L1] and [L2], currying is the transpose map $\mathcal{C}(A\times B,C)\to \mathcal{C}(A,C^B)$, and uncurrying is its inverse transpose. For any adjunction, transpose followed by inverse transpose and inverse transpose followed by transpose are the identity.

Therefore $\mathrm{uncurry}(\mathrm{curry}(f))=f$ and $\mathrm{curry}(\mathrm{uncurry}(g))=g$.

For a morphism $h:A\times B\times C\to D$, first curry in the $C$-variable and then in the $B$-variable. The resulting map $A\to (D^C{)}^B$ is the transpose of the same iterated evaluation map that produces $A\to D^{B\times C}$ after reassociating products. By [L3], these coincide under the canonical internal-hom composition isomorphism.

So currying and uncurrying are mutually inverse, and repeated currying is associative up to the canonical reassociation.

By [L1] and [L2], the functor $A\times -$ preserves the initial object, so $A\times 0$ is initial. Hence there is an isomorphism $e:A\times 0\to 0$.

The pair $(1_A,f)$ induces a morphism $⟨1_A,f⟩:A\to A\times 0$. Let $g:={\pi }_1\circ e^{-1}:0\to A$, where ${\pi }_1:A\times 0\to A$ is the first projection. Then $g\circ f={\pi }_1\circ e^{-1}\circ e\circ ⟨1_A,f⟩={\pi }_1\circ ⟨1_A,f⟩=1_A$.

The composite $f\circ g:0\to 0$ is the unique endomorphism of the initial object, so by [L3] it equals $1_0$. Thus $g$ is a two-sided inverse to $f$, and $f$ is an isomorphism.

Therefore the initial object is strict.

By [L1], the inequality $u\le v$ is the same as the existence of a morphism $u\to v$ in the associated thin category. By [L3], the product $x\times a$ is exactly the meet $x\wedge a$.

Let $b^a$ denote the exponential object given by [L2]. The adjunction $-\times a⊣(-{)}^a$ gives $\mathrm{Hom}(x\wedge a,b)\cong \mathrm{Hom}(x,b^a)$. Since each hom-set in a preorder is either empty or a singleton, this bijection says precisely that $x\wedge a\le b$ iff $x\le b^a$.

Therefore every cartesian closed preorder has the stated relative implication operation.

By [L2], the slice-of-a-slice $(\mathcal{C}\mathrm{/}X)\mathrm{/}a$ is canonically isomorphic to the ordinary slice $\mathcal{C}\mathrm{/}A$.

Since $\mathcal{C}$ is locally cartesian closed, [L1] says that $\mathcal{C}\mathrm{/}A$ is cartesian closed. Transporting this structure across the isomorphism of step 1.1 shows that $(\mathcal{C}\mathrm{/}X)\mathrm{/}a$ is cartesian closed.

Because $a$ was an arbitrary object of $\mathcal{C}\mathrm{/}X$, every slice of $\mathcal{C}\mathrm{/}X$ is cartesian closed. Hence $\mathcal{C}\mathrm{/}X$ is locally cartesian closed.

The assignment $A\mapsto {!}_A:A\to \mathbf{1}$ defines a functor $\mathcal{C}\to \mathcal{C}\mathrm{/}\mathbf{1}$, and forgetting the structure map defines a functor back. Because [L2] gives a unique map to $\mathbf{1}$, these two functors are inverse isomorphisms of categories.

By [L1], the slice $\mathcal{C}\mathrm{/}\mathbf{1}$ is cartesian closed. Transport that structure across the isomorphism of step 1.1 to conclude that $\mathcal{C}$ itself is cartesian closed.

Therefore a locally cartesian closed category with a terminal object is cartesian closed.

Fix arrows $u:A\to X$ and $v:B\to X$. Since $\mathcal{C}\mathrm{/}X$ is cartesian closed by [L1], it has a binary product $(p:P\to X)$ of those two slice objects. Its projections are morphisms $P\to A$ and $P\to B$ over $X$, and the product universal property in the slice is exactly the pullback universal property of [L2]. So $\mathcal{C}$ has pullbacks.

Now assume $\mathbf{1}$ is terminal. A pullback with codomain $\mathbf{1}$ is an ordinary binary product, because by [L3] every object has a unique map to $\mathbf{1}$. Thus step 1.1 gives binary products in $\mathcal{C}$, and the given object $\mathbf{1}$ is terminal.

A category with pullbacks and a terminal object has all finite limits: binary products come from step 2.1, and equalizers are pullbacks of the diagonal against a pair of parallel arrows. Hence $\mathcal{C}$ has all finite limits.

Therefore every locally cartesian closed category has pullbacks, and with a terminal object it has all finite limits.

Assume condition (1), fix $f:X\to Y$, and put $\mathcal{K}=\mathcal{C}\mathrm{/}Y$. For an object $a:A\to X$ of $\mathcal{C}\mathrm{/}X$, regard $a$ as a morphism ${\mathrm{\Sigma }}_{f}a\to f$ in $\mathcal{K}$. By [L1] and [L3], the category $\mathcal{K}$ is cartesian closed and has pullbacks. Form in $\mathcal{K}$ the pullback ${\mathrm{\Pi }}_f(a):=({\mathrm{\Sigma }}_{f}a{)}^f{\times }_{f^f}\mathbf{1},$ where $({\mathrm{\Sigma }}_{f}a{)}^f\to f^f$ is induced by $a$ and $\mathbf{1}\to f^f$ is the transpose of $1_f:f\to f$. For $B\to Y$, currying identifies a map $B\to ({\mathrm{\Sigma }}_{f}a{)}^f$ with a map $h:B{\times }_{Y}X\to A$ over $Y$; the pullback equation defining ${\mathrm{\Pi }}_f(a)$ says exactly that $ah$ is the projection $B{\times }_{Y}X\to X$. Hence $(\mathcal{C}\mathrm{/}Y)(B,{\mathrm{\Pi }}_f(a))\cong (\mathcal{C}\mathrm{/}X)(f^{\ast }B,a)$ naturally in $B$ and $a$. Thus $f^{\ast }$ has right adjoint ${\mathrm{\Pi }}_f$.

Assume condition (2), and fix an object $X$. Chosen pullbacks give binary products in $\mathcal{C}\mathrm{/}X$, and $1_X:X\to X$ is terminal there. For $a:A\to X$, the pullback universal property gives ${\mathrm{\Sigma }}_a⊣a^{\ast }$, while condition (2) gives $a^{\ast }⊣{\mathrm{\Pi }}_a$. The product functor with $a$ on $\mathcal{C}\mathrm{/}X$ is the composite $-{\times }_{X}a={\mathrm{\Sigma }}_a{a}^{\ast }\mathrm{.}$ Consequently it has right adjoint ${\mathrm{\Pi }}_a{a}^{\ast }$. Since this holds for every $a$, the slice $\mathcal{C}\mathrm{/}X$ is cartesian closed.

Step 1.1 proves that condition (1) implies condition (2). Step 1.2 proves that each slice $\mathcal{C}\mathrm{/}X$ is cartesian closed, so condition (2) implies condition (1). Therefore the two conditions are equivalent.

For $p:E\to X$, define a set over $Y$ by $({\mathrm{\Pi }}_{f}E{)}_y:={\prod }_{x\in f^{-1}(y)}{E}_x$, where $E_x=p^{-1}(x)$. An element of $({\mathrm{\Pi }}_{f}E{)}_y$ is therefore a choice of one element of $E_x$ for each $x$ over $y$; when $f^{-1}(y)=\mathrm{\varnothing }$, this product is the singleton empty family. The projection ${\mathrm{\Pi }}_{f}E\to Y$ sends such a family to $y$.

If $q:B\to Y$ is another object over $Y$, then a morphism $q\to {\mathrm{\Pi }}_{f}E$ over $Y$ assigns to each $b\in B$ over $y=q(b)$ a family of elements in the fibers $E_x$ for $x\in f^{-1}(y)$. Equivalently, it assigns to each pair $(b,x)$ with $q(b)=f(x)$ an element of $E_x$, which is exactly a morphism $f^{\ast }q\to p$ over $X$. This correspondence is natural and is the fiberwise form of [L3].

Step 2.1 constructs a right adjoint ${\mathrm{\Pi }}_f$ to every pullback functor in $\mathbf{S}\mathbf{e}\mathbf{t}$. Hence [L1] implies that $\mathbf{S}\mathbf{e}\mathbf{t}$ is locally cartesian closed.

By [L3], the quotient ${\mathrm{Sub}}_M(X):=M_X\mathrm{/}\sim$ by mutual factorization is a well-defined set for each $X$, and its elements correspond exactly to subobject classes of $X$ represented inside the supplied set $M_X$.

For a morphism $u:X\to Y$ and a class $[m]\in {\mathrm{Sub}}_M(Y)$, pull back $m$ along $u$. The resulting monomorphism into $X$ defines a subobject class of $X$, and [L2] provides a representative of that class in $M_X$; step 1.1 shows that the resulting element of ${\mathrm{Sub}}_M(X)$ is independent of the chosen representative. Hence $X\mapsto {\mathrm{Sub}}_M(X)$ is a contravariant functor.

For each $X$, define ${\mathrm{\Phi }}_X:\mathcal{C}(X,\mathrm{\Omega })\to {\mathrm{Sub}}_M(X)$ by sending $f:X\to \mathrm{\Omega }$ to the class of the pullback of $\mathrm{true}$ along $f$. Conversely, define ${\mathrm{\Psi }}_X:{\mathrm{Sub}}_M(X)\to \mathcal{C}(X,\mathrm{\Omega })$ by sending the class of $m$ to its unique classifying map ${\chi }_m$ from [L1].

The composites are identities. If $f:X\to \mathrm{\Omega }$, then ${\mathrm{\Psi }}_X({\mathrm{\Phi }}_X(f))=f$ because the pullback subobject of $\mathrm{true}$ along $f$ is classified by $f$ itself, and that classifying map is unique by [L1]. If $[m]\in {\mathrm{Sub}}_M(X)$, then the pullback of $\mathrm{true}$ along ${\chi }_m$ represents the same subobject class as $m$, so ${\mathrm{\Phi }}_X({\mathrm{\Psi }}_X([m]))=[m]$. Naturality follows because pullback commutes with composition of classifying maps.

Therefore $\mathrm{\Phi }$ is a natural isomorphism $\mathcal{C}(-,\mathrm{\Omega })\cong {\mathrm{Sub}}_M$. By [L4], $\mathrm{\Omega }$ represents the supplied representative-set form of the subobject functor.

By [L1] and [L2], $m$ is an injection. Its image $m[A]\subseteq X$ is a subset, and the bijection $A\to m[A]$ identifies $m$ with the inclusion $m[A]\hookrightarrow X$. Define ${\chi }_m:X\to 2$ by ${\chi }_m(x)=1$ for $x\in m[A]$ and ${\chi }_m(x)=0$ otherwise.

The pullback of $\mathrm{true}:1\to 2$ along ${\chi }_m$ has underlying set ${\chi }_m^{-1}(1)=m[A]$, so its inclusion into $X$ represents the same subobject as $m$ via the bijection from step 1.1.

If $f:X\to 2$ has a pullback representing the same subobject as $m$, then $f^{-1}(1)=m[A]$, so $f$ agrees pointwise with ${\chi }_m$. Hence the classifying map is unique. By [L3], $\mathrm{true}:1\to 2$ is a subobject classifier.