4
$\begingroup$

In this discussion from the categories mailing there is mention of the following result by Robin Houston, supposedly proved in 2006:

Theorem. Let $\mathcal{C}$ be a symmetric closed monoidal category, and let $D$ be an object. If there exists a natural isomorphism $f : A \rightarrow (A \multimap D) \multimap D$, then the canonical natural transformation $g : A \rightarrow (A \multimap D) \multimap D$ (coming from the symmetric closed monoidal structure) is an isomorphism (although it may in general be different from $f$).

In the quoted text the term "closed" is missing. Without it, the passage does not seem to make much sense, so I added it in.

I have skimmed through Robin Houston's papers (especially the 2005 paper entitled "Modelling Linear Logic Without Units (Preliminary Results)" seems relevant), but could not find the result in question. Does someone know a reference?

$\endgroup$
1
  • 3
    $\begingroup$ Perhaps it would be worth contacting Robin Houston? I notice another result about monoidal categories is attributed to him on the nLab page for semicartesian categories, but without a proof. Perhaps he could be persuaded to write these up. $\endgroup$
    – varkor
    Commented Nov 29, 2023 at 12:09

1 Answer 1

9
$\begingroup$

This is a special case of:

Let $F\dashv G$ be an adjunction. If there exists an isomorphism $id \cong GF$, then the unit $id \to GF$ is an isomorphism.

Indeed, $[-,A]$ is left adjoint to itself as one can check by puttingop's in the appropriate places.

I believe this result is proved in Johnstone's Sketches of an elephant, or at least I've been told it was. But the proof is rather simple, and in fact this is in turn a special case of:

Let $M$ be a monoidal category, and $A$ an algebra in $M$. If the underlying object of $A$ is isomorphic in $M$ to the unit $\mathbf{1}_M$, then the unit map $\mathbf{1}_M \to A $ is an isomorphism.

You can then apply this to the monoidal category of endofunctors: there, $GF$ is an algebra (i.e. $GF$ is a monad).

This statement, in turn, can be proved by some diagram chasing.Unwinding the proof in the special case sounds daunting.

$\endgroup$
6
  • $\begingroup$ Very nice interpretation. In other words, the unit object has a unique monoid structure. This is rather easy for strict monoidal categories (not sure if coherence thm then implies it in general, or if we only get uniqueness up to isomorphism), and these are the ones we need for applying it to monads. $\endgroup$ Commented Nov 29, 2023 at 23:23
  • 1
    $\begingroup$ @MartinBrandenburg : yes the coherence theorem implies it in general - but you can also prove it directly in an arbitrary monoidal category :) $\endgroup$ Commented Nov 30, 2023 at 8:00
  • $\begingroup$ An explicit proof: Let $(\mu,\eta)$ be a unital monoid structure on the monoidal unit $I$. Since for the unitors we have $\lambda_I=\rho_I$ (one can use Mac Lane's coherence theorem or give an elementary proof), unitality of the monoid implies $\mu\circ (\eta\otimes \operatorname{id}_I)\circ {\rho_I}^{-1}=\operatorname{id}_I$. By naturality of the right unitor, this is equivalent to $\mu \circ {\rho_I}^{-1}\circ \eta=\operatorname{id}_I$ … $\endgroup$ Commented Dec 13, 2023 at 15:46
  • $\begingroup$ … By the Eckmann-Hilton argument, the endomorphism monoid $\operatorname{End}(I)$ is commutative, thus we also have $\eta\circ \mu \circ {\rho_I}^{-1}=\operatorname{id}_I$ and $\eta$ is invertible. Since any monoid $(A,m,e)$ together with an isomorphism $f:A\rightarrow I$ induces a monoid structure on $I$ whose unit is given by $f\circ e$ (transport of structure), this finishes the proof. $\endgroup$ Commented Dec 13, 2023 at 15:46
  • $\begingroup$ @MartinBrandenburg: The monoid structure on the monoidal unit is not strictly unique. For instance, let $k$ be a field with more than two elements and consider the category of $k$-vector spaces with its usual monoidal structure. Pick an invertible element $x\in k$ different from $1$. Then for the canonical monoid structure $(\mu,\eta)$ on the monoidal unit $k$, the pair $(x\cdot \mu, x^{-1}\cdot \eta)$ gives a different (though isomorphic) monoid structure… $\endgroup$ Commented Dec 13, 2023 at 15:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .