Tensor products from internal hom?
Monoidal categories come with tensor products, and sometimes, these categories are biclosed, i.e each restriction of the tensor bifunctor has a right adjoint. If the category happens to be symmetric, then restrictions of the $\otimes$ bifunctor are naturally isomorphic and we can talk about symmetric monoidal closed categories.
If I understand correctly, the internal hom is precisely this right adjoint to $-\otimes A$. Hence, the internal hom comes from $\otimes$ and not the other way around.
(When) Is it possible to first define the internal hom, and then have it induce $\otimes$ from the adjunction? Can we somehow go the other way around and get monoidal structure from somehow defining an internal hom?
Solution 1:
In general if you don't want to start with the monoidal structure, you start with a closed category. In a closed category $\mathsf C$, you have a bifunctor $$[-,-] : \mathsf C^{op} \times \mathsf C \to \mathsf C,$$ called the internal hom, and various other data that are somewhat "dual" to the axioms of a monoidal category (I put dual in quotes because this isn't the dual notion of "monoidal category", you just dualize one side of the bifunctor $- \otimes -$ to get the axioms for $[-,-]$). More specifically:
- a unit object $I$,
- a natural isomorphism $\operatorname{id}_{\mathsf C} \cong [I, -]$,
- an extranatural transformation $j_X : I \to [X, X]$ that corresponds to getting the "identity" in $[X,X]$,
- post-composition transformation $[Y,Z] \to [[X,Y], [X,Z]$,
subject to various coherence conditions.*
Then just like the internal hom $[-,X]$ in a monoidal category, if it exists, is the right adjoint to $- \otimes X$, the tensor product in a closed category is the left adjoint to the internal hom (if it exists). In both cases you get a closed monoidal category. It's also possible to define categories enriched over closed categories, in a manner similar to categories enriched over a monoidal category, and the two notions coincide when the category is closed monoidal.
* These data are truly dual to the data you want for a monoidal category. Take the point of view that $\hom(X \otimes Y, Z) \cong \hom(X, [Y,Z])$ as if you were truly in a closed monoidal category. Then you can use the Yoneda embedding to make the correspondence clear:
- The isomorphism $[I, X] \cong X$ becomes $\hom(Y, [I,X]) \cong \hom(Y \otimes I, X)$ naturally in $X$ and $Y$, so you get the right unitor $- \otimes I \cong \operatorname{id}_{\mathsf C}$.
- The transformation $I \to [X,X]$ becomes a transformation $$\hom(Y, I) \to \hom(Y, [X,X]) \cong \hom(Y \otimes X, X).$$ If you take $Y = I$ you get $\hom(I,I) \to \hom(I \otimes X, X)$, and the image of the identity of $I$ because the left unitor.
- The data of the associator is equivalent to an (extra in some variables)natural isomorphism $[A, [B,C]] \cong [A \otimes B, C]$. The relation with the post-composition is trickier and I'll let you peruse the reference.
Of course none of the above is an actual proof, just a sketch of the ideas that go into this. Proofs can be found in:
Kelly, G. Max; Mac Lane, Saunders, Coherence in closed categories. J. Pure Appl. Algebra 1 1971 no. 1, 97–140. doi: 10.1016/0022-4049(71)90013-2.
Solution 2:
This is only a small addition to Najib's very nice answer which is nevertheless too long for a comment.
It is even interesting to look at the structure of a closed category in the following very restricted setting:
- We consider only posets $({\mathsf P},\leq)$ considered as a categories.
- We consider only those closed structures in which the unit is a terminal object (intuitively, these are like the internal homs corresponding to the categorical product $\times$ as the monoidal structure)
Denoting ${\mathsf T}$ the terminal object of ${\mathsf P}$, $[-,-]$ is then a function $\to: ({\mathsf P},\leq)^{\text{op}}\times ({\mathsf P},\leq)\to({\mathsf P},\leq)$ such that:
For all $P\in{\mathsf P}$ we have $({\mathsf T}\to P) = P$ and ${\mathsf T}\leq (P\to P)$, i.e. $(P\to P) = {\mathsf T}$.
For all $P,Q,R\in{\mathsf P}$ we have $(Q\to R)\leq ((P\to Q)\to (P\to R))$.
This already looks very 'logical', and indeed: Taking ${\mathsf P}$ to be the equivalence classes of formulae in the implicational fragment of intuitionistic propositional logic, with $\to$ being given by $[\psi]\to[\phi] := [\psi\Rightarrow\phi]$, satisfies these axioms.
On the $1$-categorical level, you find an interesting example by looking at the category which again has implicational propositional formulae as objects but equivalence classes of proofs - in the sense of terms in simply typed $\lambda$-calculus - as morphisms. Note that in this setting there is really no categorical product present, but only the internal hom given by implication.
See also http://www.moravica.ftn.kg.ac.rs/Vol_3/04-Dudek.pdf