Todd Trimble Closed structure on modules over a commutative monoid

User “Buschi Sergio” at MathOverflow referred to a remark given in a paper by Stefan Schwede and Brooke Shipley (which, according to a comment by David White, the authors credit to Charles Rezk):

Theorem

Let $C$ be a complete, cocomplete, symmetric monoidal closed category, and let $R$ be a commutative monoid with respect to the symmetric monoidal product. Then the category $Mod_R$ of left $R$ -modules carries (under the expected definitions) a symmetric monoidal closed structure.

We will denote the monoidal product in $C$ by $\otimes$ , the symmetry isomorphism by $c$ , and the internal hom in $C$ by $[-, -]$ .

A full proof of this, starting from scratch and proceeding in a hands-on way, is somewhat long-winded. But, let’s start from the evident construction of the internal hom for $Mod_R$ , which for two left $R$ -modules $M$ , $N$ (with actions denoted $\alpha \colon R \otimes M \to M$ and $\beta \colon R \otimes N \to N$ ) is given by an equalizer diagram in $C$

[M, N]_R \to [M, N] \stackrel{\overset{[\alpha, 1_N]}{\to}}{\underset{\beta'}{\to}} [R \otimes M, N]

where $\beta'$ is the evident composite

[M, N] \stackrel{\phi}{\to} [R \otimes M, R \otimes N] \stackrel{[1, \beta]}{\to} [R \otimes M, N].

Buschi Sergio’s specific question (see below) was then how to prove (or how to find a reference for) the assertion that $[M, N]_R$ (the putative internal hom in $Mod_R$ ) is realized as living in $Mod_R$ . As I said in my answer, the basic idea is to restrict an evident¹ $R$ -module structure on $[M, N]$ (induced from $\beta$ ; see below) to the subobject $[M, N]_R$ .

In my answer, I claimed that the assertion should be seen as essentially “obvious”, and that it can be proven more or less as it would be in the familiar case where $C = Ab$ , where we can just rely on elements. I had also written down a sequence of equations between terms that suggest an elements-based proof of this claim:

(r f)(s m) \stackrel{def}{=} r(f (s m)) = r(s f(m)) = (r s)(f(m)) = (s r)(f(m)) = s(r f(m)) \stackrel{def}{=} s((rf)(m))

I still stand by what I said, but before continuing, two remarks:

Ultimately it is justifiable (if a bit hand-wavy) to say that these equations provide a scaffold for a proof in the general case. There are various formalisms for effecting the transition between the elementwise approach and a general proof using commutative diagrams, using one of various “languages for monoidal categories” (e.g., Barry Jay’s). Indeed, one can develop a lambda-calculus adapted to multiplicative intuitionistic linear logic (MILL), and translate the equations above into equations between such lambda terms, and then invoke soundness and completeness of that lambda calculus for MILL to prove theorems in the language of smc categories. But possibly such meta-theory will not satisfy readers who want a more hands-on approach.
The theorem itself is a special case of a much more general result, tracing back to early work of Anders Kock on commutative monads (which Buschi Sergio recognizes, but apparently doesn’t want to rely on).

In the end, I decided it might be more satisfactory to Buschi Sergio if I stopped waving my hands and instead got them dirty. Okay then, I’ll bite the bullet and give a hands-on proof via commutative diagrams.

Kelly-Mac Lane theorem

I would like to permit myself one luxury, however: the Kelly-Mac Lane theorem which gives a simple criterion for commutativity for a large class of diagrams in symmetric monoidal closed categories. This theorem is about diagrams in free symmetric monoidal closed categories generated by a set $X$ of letters, in which objects are formal expressions constructed by starting with letters in $X$ and forming words using $\otimes$ and $[-, -]$ . We must also include a constant $I$ standing for the monoidal unit, but for the form of the Kelly-Mac Lane theorem which we will use, we are only concerned with words in which $I$ does not occur. Such words will be called unit-free. Letter-occurrences in a word $X$ form a multi-set denoted $var(X)$ ; unions of such multi-sets formed by adding multiplicities are denoted $var(X) + var(Y)$ .

Theorem (Kelly-Mac Lane)

Let $F = F[a, b, c, \ldots]$ be the free symmetric monoidal closed category generated by a countably infinite set of letters. Let $f, g \colon X \to Y$ be morphisms in $F$ between unit-free words where each letter occurring in $var(X) + var(Y)$ occurs exactly twice. Then $f = g$ .

For example, by this theorem there is exactly one morphism in $F$ of shape

[b, a] \otimes b \to a

(namely the internal evaluation map). In this example, the morphism is natural in the variable $a$ and extranatural in the variable $b$ ; in general, the two occurrences of each letter appearing in the domain/codomain of such “every-variable-twice” morphisms are connected via naturality or extranaturality, so the theorem roughly says that any two smc-definable transformations having the same (extra)natural form must be equal – a kind of coherence theorem.

The typical way this theorem is applied is where one considers two legs of a diagram, in a general smc category $V$ , formed from the smc data of $V$ , and one recognizes one leg as an instantiation or value of a morphism $f colon X \to Y$ under an smc functor $\Phi \colon F[a, b, c, \ldots] \to V$ (uniquely determined by assigning object-values in $V$ to letters), and the other leg as an instantiation $\Phi(g)$ under the same $\Phi$ . If $f$ and $g$ have the same unit-free domain and codomain and are every-variable-twice, the diagram commutes.

$[M, N]_R$ as an $R$ -module

Thus far, we have an enrichment

[-, -]_R \colon Mod_R^{op} \times Mod_R \to C

which we want to lift through the monadic functor $Mod_R \to C$ . Recall that given an $R$ -module $N$ , there is a canonical $R$ -module structure on $[M, N]$ given by

R \otimes [M, N] \to [M, R \otimes N] \stackrel{[M, \beta]}{\to} [M, N]

where the first map is evident. (Indeed, in any smc category there is a canonical map

a \otimes [b, c] \to [b, a \otimes c]

natural in the three variables $a, b, c$ .) We wish to show that the $R$ -action on $[M, N]$ restricts to an $R$ -action on $[M, N]_R$ .

We thus consider the following diagram (where $\phi$ and $\psi$ are “evident” maps; $\psi$ expresses enriched functoriality of $R \otimes -$ ):

\array{ R \otimes [M, N]_R & & \stackrel{?}{\to} & & [M, N]_R & & \\ \mathllap{1 \otimes i} \downarrow & & & & \downarrow \mathrlap{i} & & \\ R \otimes [M, N] & \stackrel{\phi}{\to} & [M, R \otimes N] & \stackrel{[1, \beta]}{\to} & [M, N] & & \\ & \searrow \mathrlap{1 \otimes \psi} & & & & \searrow \mathrlap{\psi} & \\ \mathllap{1 \otimes [\alpha, 1]} \downarrow & & R \otimes [R \otimes M, R \otimes N] & & \mathllap{[\alpha, 1]} \downarrow & & [R \otimes M, R \otimes N] \\ & \swarrow _\mathrlap{1 \otimes [1, \beta]} & & & & \swarrow _\mathrlap{[1, \beta]} & \\ R \otimes [R \otimes M, N] & \underset{\phi}{\to} & [R \otimes M, R \otimes N] & \underset{[1, \beta]}{\to} & [R \otimes M, N] & & }

Theorem

Given that $i$ is the equalizer of the two maps $[M, N] \to [R \otimes M, N]$ shown, the composite $[1, \beta] \circ \phi \circ (1 \otimes i)$ equalizes those two maps (and therefore factors through $i$ , yielding the arrow indicated by the ? symbol that is to be the $R$ -action on $[M, N]_R$ ).

Lemma

The rectangle expressed by the equation

[\alpha, 1] \circ [1, \beta] \circ \phi = [1, \beta] \circ \phi \circ (1 \otimes [\alpha, 1])

commutes.

Proof

The left rectangle in the diagram

\array{ R \otimes [M, N] & \stackrel{\phi}{\to} & [M, R \otimes N] & \stackrel{[1, \beta]}{\to} & [M, N] \\ \mathllap{1 \otimes [\alpha, 1]} \downarrow & & \mathllap{[\alpha, 1]} \downarrow & & \downarrow \mathrlap{[\alpha, 1]} \\ R \otimes [R \otimes M, N] & \underset{\phi}{\to} & [R \otimes M, R \otimes N] & \underset{[1, \beta]}{\to} & [R \otimes M, N] }

commutes by (extra)naturality of $\phi_{a, b, c} \colon a \otimes [b, c] \to [b, a \otimes c]$ . The right rectangle commutes by functoriality of $[-, -]$ .

Referring back to the diagram in the theorem, it follows that

(1)

\array{ [\alpha, 1] \circ [1, \beta] \circ \phi \circ (1 \otimes i) & = & [1, \beta] \circ \phi \circ (1 \otimes [\alpha, 1]) \circ (1 \otimes i) \\ & = & [1, \beta] \circ \phi \circ (1 \otimes [1, \beta]) \circ (1 \otimes \psi) \circ (1 \otimes i) }

where the second equation uses functoriality of $1 \otimes -$ and the fact that $i$ equalizes the pair $([\alpha, 1], [1, \beta] \circ \psi)$ .

Lemma

The following diagram commutes:

\array{ & & R \otimes [M, N] & \stackrel{\phi}{\to} & [M, R \otimes N] \\ & \mathllap{1 \otimes \psi} \swarrow & & & \downarrow \mathrlap{\psi} \\ R \otimes [R \otimes M, R \otimes N] & \underset{\phi}{\to} & [R \otimes M, R \otimes R \otimes N] & \underset{[1, c \otimes 1]}{\to} & [R \otimes M, R \otimes R \otimes N] }

Proof

By the Kelly-Mac Lane theorem. Both legs of the diagram are instances of maps of the form

a \otimes [b, c] \to [d \otimes b, d \otimes a \otimes c]

(substituting $R$ for $a$ and $d$ , $M$ for $b$ , and $N$ for $c$ ), so the diagram commutes.

Lemma

The following diagram commutes, where $m \colon R \otimes R \to R$ is the multiplication on the commutative monoid $R$ :

\array{ & & R \otimes [M, N] & \stackrel{\phi}{\to} & [M, R \otimes N] & \stackrel{[1, \beta]}{\to} & [M, N]\\ & \mathllap{1 \otimes \psi} \swarrow & & & \downarrow \mathrlap{\psi} & & \downarrow \mathrlap{\psi} \\ R \otimes [R \otimes M, R \otimes N] & \underset{\phi}{\to} & [R \otimes M, R \otimes R \otimes N] & \underset{[1, c \otimes 1]}{\to} & [R \otimes M, R \otimes R \otimes N] & \underset{[1, 1 \otimes \beta]}{\to} & [R \otimes M, R \otimes N] \\ & & & \mathllap{[1, m \otimes 1]} \searrow & \downarrow \mathrlap{[1, m \otimes 1]} & & \downarrow \mathrlap{[1, \beta]} \\ & & & & [R \otimes M, R \otimes N] & \underset{[1, \beta]}{\to} & [R \otimes M, N] }

Proof

The upper left diagram commutes by the preceding lemma. The upper right square commutes by naturality of $\psi$ . The lower triangle commutes by commutativity of the monoid $R$ (and functoriality of $[1, - \otimes 1]$ ). The lower square commutes by the associativity condition on the action $\beta \colon R \otimes N \to N$ (and by functoriality of $[1, -]$ ).

Proof of Theorem 1

Recall that we are trying to show

[\alpha, 1] \circ [1, \beta] \circ \phi \circ (1 \otimes i) = [1, \beta] \circ \psi \circ [1, \beta] \circ \phi \circ (1 \otimes i).

The first equation below picks up where we left off in equation (1)

\array{ [\alpha, 1] \circ [1, \beta] \circ \phi \circ (1 \otimes i) & = & [1, \beta] \circ \phi \circ (1 \otimes [1, \beta]) \circ (1 \otimes \psi) \circ (1 \otimes i) & & \\ & = & [1, \beta] \circ [1, 1 \otimes \beta] \circ \phi \circ (1 \otimes \psi) \circ (1 \otimes i) & & (naturality \; of \; \phi)\\ & = & [1, \beta] \circ [1, m \otimes 1] \circ \phi \circ (1 \otimes \psi) \circ (1 \otimes i) & & (associativity \; of \; \beta)\\ & = & [1, \beta] \circ \psi \circ [1, \beta] \circ \phi \circ (1 \otimes i) & & (by \; preceding \; lemma) }

which completes the proof.

From there, given the action $R \otimes [M, N]_R \to [M, N]_R$ thus produced, it is routine that the module axioms are satisfied, since the module equations hold on the action $R \otimes [M, N] \to [M, N]$ and we are simply restricting that action.

References

Buschi Sergio (mathoverflow.net/users/6262), About the closed structure on the modules of a monoidal closed symmetrical category, http://mathoverflow.net/questions/114457 (version: 2012-11-26)

C.B. Jay, Languages for monoidal categories, J. Pure Appl. Alg., vol. 59 (1989), 61-85.

G.M. Kelly and S. Mac Lane, Coherence in closed categories, J. Pure Appl. Alg., vol. 1 (1971), 97-140.

All uses of the word “evident” indicate that something is being left to the reader. Usually that something is labeled by a nondescript Greek letter like $\phi$ . ↩

Revised on November 28, 2012 at 21:33:14 by Todd Trimble

Todd Trimble Closed structure on modules over a commutative monoid

Theorem

Kelly-Mac Lane theorem

Theorem (Kelly-Mac Lane)

[M,N] R[M, N]_R as an RR-module

Theorem

Lemma

Proof

Lemma

Proof

Lemma

Proof

Proof of Theorem 1

References

$[M, N]_R$ as an $R$ -module