Strict monoidal models and transport of algebra objects

Written by GPT-6.1 Sol (OpenAI), October 2026. Public domain (CC0).

Parentheses can be normalized while every original morphism remains available. The resulting strict category has words as objects, but its arrows are all maps between their evaluated tensor products. This distinguishes a strict model of a given category from the free category whose arrows act separately on letters.

Work with a locally small monoidal category \(\mathcal C\) in suitable fixed universes, enlarging the object universe when necessary. Write \(I\) for its unit and \(a:(X\otimes Y)\otimes Z\to X\otimes(Y\otimes Z)\), \(l\) and \(r\) for its constraints. No braiding, additivity or exactness is assumed. We use the independent normal-form coherence proof described in Tensor actions, Section 1: its pinned Mathlib proof constructs a natural normalization isomorphism and proves equality of parallel formal structural maps. That proof does not assume the strictification constructed here. It applies to the same ordered formal letters and unit insertions; it does not identify arbitrary arrows with equal evaluated endpoints. The free tensor-word lesson supplies the comparison with the letterwise free construction.

1. Evaluation and the concatenation comparisons

For a finite word \(u=(X_1,\ldots,X_n)\), evaluate with left association: \[ \begin{gathered}E[]=I,\qquad E[X]=X,\\ E(u[X])=Eu\otimes X\quad(u\ne[]).\end{gathered} \tag{1.1} \] The empty word is a genuine object, distinct from the one-letter word \([I]\). Concatenation is written \(uv\).

Choose the structural isomorphism \[ \mu_{u,v}:Eu\otimes Ev\longrightarrow E(uv). \tag{1.2} \] For empty factors use \(\mu_{[],v}=l_{Ev}\) and \(\mu_{u,[]}=r_{Eu}\); for both empty these agree because \(l_I=r_I\). For nonempty factors, reassociate the ordered factors to their left-associated evaluation. Coherence makes every such choice equal; in particular \(\mu_{[X],[Y]}=1_{X\otimes Y}\).

Lemma 1.1 (the split identity). For any three words, \[ \begin{gathered} \mu_{uv,w}(\mu_{u,v}\otimes1)\\ =\mu_{u,vw}(1\otimes\mu_{v,w})\\ \cdot a_{Eu,Ev,Ew}. \end{gathered} \tag{1.3} \] Proof. Both sides are structural maps from \((Eu\otimes Ev)\otimes Ew\) to the left-associated evaluation of the same concatenated word. Replace each occurrence of an evaluated nonempty word by its ordered formal letters and each empty word by a formal unit. The independent coherence theorem makes the two formal composites equal, and evaluation gives (1.3). This includes every empty-factor case and the identity \(l_I=r_I\). Naturality of all these maps follows from naturality of the associator and unit maps, by composition and tensoring. \(\square\)

2. A strict category with all the original arrows

Let \(\mathcal W\mathcal C\) have finite words as objects, and define \[ \operatorname{Hom}_{\mathcal W\mathcal C}(u,v) =\operatorname{Hom}_{\mathcal C}(Eu,Ev). \tag{2.1} \] Identity and composition are those in \(\mathcal C\). This is a category because their types, associativity and units are inherited exactly; its Hom collections are small. Define tensor on objects by concatenation. For \(f:u\to u'\) and \(g:v\to v'\), define its arrow by \[ \begin{gathered}f\mathbin{\Box}g\\ =\mu_{u',v'}(f\otimes g)\mu_{u,v}^{-1}.\end{gathered} \tag{2.2} \]

Theorem 2.1. These operations make \(\mathcal W\mathcal C\) a strict monoidal category, with empty word as unit. Evaluation \(E:\mathcal W\mathcal C\to\mathcal C\), identity on each Hom set, is a strong monoidal equivalence with tensor comparison \(\mu\) and unit comparison \(1_I\).

Proof: tensor is a bifunctor. Tensoring identity arrows in (2.2) gives identity. For successive pairs of arrows, the adjacent inverse and forward \(\mu\)'s cancel. Bifunctoriality of the original tensor then gives \[ \begin{gathered}(f'f)\Box(g'g)\\ =(f'\Box g')(f\Box g).\end{gathered} \tag{2.3} \] Thus this is a bifunctor, not just an operation on isomorphisms.

Proof: strict associativity. Expanding \((f\Box g)\Box h\) gives the composite through \((Eu\otimes Ev)\otimes Ew\), with the outer comparisons \[ \mu_{uv,w}(\mu_{u,v}\otimes1) \tag{2.4} \] at source and target. Expanding \(f\Box(g\Box h)\) gives the corresponding comparisons through \(Eu\otimes(Ev\otimes Ew)\). Identity (1.3) changes the first comparisons into the second with an associator inserted. Naturality of that associator moves \((f\otimes g)\otimes h\) to \(f\otimes(g\otimes h)\); the source inverse cancels the remaining associator. The two arrows are therefore equal. Their source and target words are literally equal by associativity of concatenation. Consequently the associator of \(\mathcal W\mathcal C\) is identity.

Proof: strict units and evaluation. The left empty-word tensor of \(f:u\to v\) is \(l_{Ev}(1_I\otimes f)l_{Eu}^{-1}=f\), by naturality of \(l\). The right calculation uses \(r\) and gives the same conclusion. Hence both unit constraints are identity on arrows as well as objects. Equation (2.2) is exactly naturality of the tensor comparison for \(E\), and (1.3) is its associativity axiom. Its two unit axioms are the definitions of \(\mu_{[],u}\) and \(\mu_{u,[]}\). Thus \(E\) is strong monoidal. It is fully faithful by (2.1), and every \(X\) is the evaluation of \([X]\), proving essential surjectivity. \(\square\)

For an explicit inverse, let \(JX=[X]\) and let \(Jf=f\) as a singleton-word arrow. Its tensor comparison \([X,Y]\to[X\otimes Y]\) is represented by \(1_{X\otimes Y}\); its unit comparison \([]\to[I]\) is represented by \(1_I\). These maps satisfy the strong functor axioms: applying the faithful \(E\) reduces associativity to the canonical reassociations of the three original factors, and reduces the unit equations to the original unit constraints. The composite \(EJ\) is the identity strong monoidal functor.

There is a natural monoidal isomorphism \[ \begin{gathered}\kappa:1_{\mathcal W\mathcal C}\longrightarrow JE,\\ \kappa_u:u\to[Eu]\end{gathered} \tag{2.5} \] represented by \(1_{Eu}\). Naturality follows because \(\kappa_v f=[f]\kappa_u\) has representative \(f\) on both sides. For tensor compatibility, both routes from \(uv\) to \([E(uv)]\) are represented by \(1_{E(uv)}\): the transported tensor of the two identity representatives introduces precisely the \(\mu_{u,v}^{-1}\) canceled by the comparison of \(JE\). At the empty word its component is the specified unit comparison. This proves a monoidal equivalence, with its maps and inverse, rather than only an equivalence of underlying categories.

3. Strong functors become strict on word models

Let \(F:\mathcal C\to\mathcal D\) be strong monoidal, with comparisons \[ \begin{gathered} F_2:FX\otimes FY\longrightarrow F(X\otimes Y),\\ F_0:I_{\mathcal D}\longrightarrow F(I_{\mathcal C}). \end{gathered} \tag{3.1} \] Define isomorphisms \(\phi_u:E_{\mathcal D}(Fu)\to F(E_{\mathcal C}u)\). At the empty word use \(F_0\), at a singleton use identity, and for a nonempty word followed by a letter use \[ \phi_{u[X]}=F_2(\phi_u\otimes1_{FX}). \tag{3.2} \] These are invertible because every factor is invertible.

Lemma 3.1 (comparison across a split). For all words, \[ \begin{aligned} \phi_{uv}\mu^{\mathcal D}_{Fu,Fv} &=F(\mu^{\mathcal C}_{u,v})F_2\\ &\hspace{10mm}\cdot(\phi_u\otimes\phi_v). \end{aligned} \tag{3.3} \] Proof. If either word is empty, the equation is the corresponding unit axiom of the strong monoidal functor, with naturality of the unit constraint and the definition of \(F_0\). For nonempty words, induct on the length of \(v\). Length one is (3.2), since evaluation of a word followed by one letter has the prescribed left association. For the step \(v=t[X]\), expand \(\phi_{ut[X]}\) by (3.2) and apply the induction hypothesis to \(u,t\). The associativity axiom for \(F_2\) changes the resulting comparison of \((F(Eu)\otimes F(Et))\otimes FX\) into the comparison through \(F(Eu)\otimes(F(Et)\otimes FX)\). The two original \(\mu\)'s are changed in exactly this way by (1.3). Naturality of \(F_2\) then moves \(\phi_t\) and the last identity inside, leaving the right-hand side of (3.3). This proves the step and all cases. \(\square\)

Define \(\mathcal WF\) letterwise on objects and, for an arbitrary word arrow, by \[ \begin{gathered}(\mathcal WF)(f)=\phi_v^{-1}F(f)\phi_u,\\ f:u\to v.\end{gathered} \tag{3.4} \] It respects identity and composition by cancellation of adjacent \(\phi\)'s. It preserves the empty word and concatenation literally. To check tensor on arrows, substitute (2.2) into (3.4) and use (3.3) once at the source and once at the target. The remaining middle expression is \(F_2^{-1}F(f\otimes g)F_2=F(f)\otimes F(g)\), by naturality of \(F_2\). Formula (2.2) in \(\mathcal W\mathcal D\) is exactly the result. Thus \(\mathcal WF\) is a strict monoidal functor. The maps \(\phi_u\) give a monoidal natural isomorphism \(E_{\mathcal D}\mathcal WF\simeq FE_{\mathcal C}\); its naturality is (3.4) and its tensor equation is (3.3).

Every monoidal natural transformation is retained. For a monoidal natural transformation \(\alpha:F\to G\), set \[ \begin{gathered}(\mathcal W\alpha)_u\\ =(\phi^G_u)^{-1}\alpha_{E_{\mathcal C}u}\phi^F_u.\end{gathered} \tag{3.5} \] Naturality follows by inserting (3.4) on each side and applying naturality of \(\alpha\). Its component at the empty word is identity because \(\alpha_I F_0=G_0\). The tensor equation for \(\alpha\), together with (3.3), gives \((\mathcal W\alpha)_{uv}=(\mathcal W\alpha)_u\Box(\mathcal W\alpha)_v\). Hence it is a monoidal transformation between strict functors. Cancellation shows that identities and vertical composites are preserved. No component of \(\alpha\) was assumed invertible.

4. The universal property for strict targets

Let \(\mathcal D\) be strict monoidal. Write \(\mathsf{StrMon}\) for strict monoidal functors with monoidal natural transformations, and \(\mathsf{StrongMon}\) for strong monoidal functors with the same kind of transformations.

Theorem 4.1. Restriction along \(J\) gives an equivalence \[ \begin{gathered}\mathsf{StrMon}(\mathcal W\mathcal C,\mathcal D)\\ \simeq\mathsf{StrongMon}(\mathcal C,\mathcal D).\end{gathered} \tag{4.1} \] Proof. For strong \(F\), use \(\overline F=E_{\mathcal D}\mathcal WF\). Evaluation in a strict category is strict, since all its \(\mu\)'s are identity, so this is a strict functor. Use (3.5) on transformations. On single letters the formula recovers \(F\) exactly; on the comparison \([X,Y]\to[X\otimes Y]\) it recovers \(F_2\), because \(\phi_{[X,Y]}=F_2\) and the representative is identity. On \([]\to[I]\) it recovers \(F_0\). Thus \(\overline FJ\) has precisely the original strong structure, including its unit.

Conversely let \(H:\mathcal W\mathcal C\to\mathcal D\) be strict and put \(F=HJ\). Strictness gives \(\overline F(u)=H(u)\) on objects, since every word is the concatenation of its singletons. The recursive definition (3.2) now gives \(\phi_u=H(\kappa_u)\); this follows first for empty and singleton words, and then from the tensor comparison of \(HJ\). For \(f:u\to v\), naturality of \(\kappa\) says \[ [f]\kappa_u=\kappa_v f. \tag{4.2} \] Applying \(H\) and substituting into (3.4) gives \(\overline{HJ}(f)=H(f)\). Finally a monoidal transformation between strict functors has on a word the tensor product of its components on the letters, and has identity component at the empty word. Its restriction therefore determines it; formula (3.5) reconstructs those components, by (4.2) and naturality. These are mutually inverse constructions on functors and transformations, proving (4.1). \(\square\)

5. Transporting algebras and all their modules

An algebra object has multiplication \(m:A\otimes A\to A\) and unit \(e:I\to A\), satisfying the associativity and unit diagrams. A left module has action \(s:A\otimes M\to M\), with the corresponding action and unit diagrams. These definitions make sense without an additive category.

Proposition 5.1. A strong monoidal functor sends these structures to \[ \begin{gathered} \widetilde m=F(m)F_2,\\ \widetilde e=F(e)F_0,\\ \widetilde s=F(s)F_2. \end{gathered} \tag{5.1} \] If its underlying functor is an equivalence, it induces an equivalence of algebra categories, and for each \(A\) an equivalence of the full left-module categories over \(A\) and \(FA\).

Proof: laws and maps. From \((FA\otimes FA)\otimes FA\), expanding the left associativity route for \(\widetilde m\) gives \[ \begin{gathered}F(m)F(m\otimes1)\\ \cdot F_2(F_2\otimes1).\end{gathered} \tag{5.2} \] Naturality of \(F_2\) justifies the expansion. The other route expands through \(FA\otimes(FA\otimes FA)\). The associativity axiom of \(F\) identifies the comparison into \(F(A\otimes(A\otimes A))\) with \(F(a)\) followed after the comparison into \(F((A\otimes A)\otimes A)\). The original equation \(m(m\otimes1)=m(1\otimes m)a\) now proves equality. Replacing the third \(A\) by \(M\) gives exactly the action calculation. For the left unit, naturality changes the inserted \(F(e)F_0\) into \(F(e\otimes1)F_2(F_0\otimes1)\); the original unit equation and the left unit axiom of \(F\) reduce the result to the target left unitor. The right algebra unit uses the right unit axiom in the same way. For a structure-preserving arrow, naturality of \(F_2\) and functoriality carry its multiplication or action equation to the transported equation. Thus (5.1) defines the asserted functors on all morphisms.

Proof: full faithfulness and lifting objects. Assume \(F\) is fully faithful and essentially surjective. Every arrow \(FA\to FB\) is \(Fh\) for a unique \(h\). Its transported multiplication and unit equations, after canceling the invertible comparisons and using naturality, are exactly the images of the equations for \(h\). Faithfulness reflects those equations. This proves full faithfulness on algebras; the action equation proves it for modules too.

For an algebra \(B\) in the target choose an isomorphism \(t:FA\to B\). Fullness uniquely lifts \[ \begin{gathered} F(m)=t^{-1}m_B(t\otimes t)F_2^{-1},\\ F(e)=t^{-1}e_BF_0^{-1}. \end{gathered} \tag{5.3} \] Applying \(F\) to each required law and inserting these formulas reduces it to the corresponding law of \(B\), conjugated by the comparisons in (5.2). Faithfulness proves the laws in the source, and \(t\) is an algebra isomorphism. For a module \(N\) over the fixed algebra \(FA\), choose \(v:FM\to N\) invertible and lift \[ \begin{gathered}F(s)=v^{-1}s_N(1_{FA}\otimes v)\\ \cdot F_2^{-1}.\end{gathered} \tag{5.4} \] The same action and unit calculation, now with the algebra fixed, proves the lifted laws and makes \(v\) a module isomorphism. This proves both essential-surjectivity statements. \(\square\)

Applied to \(E\), this shows that strictification preserves algebras and module categories with every morphism. The singleton algebra \([A]\) has multiplication \([A,A]\to[A]\) represented by \(m\), and unit \([]\to[A]\) represented by \(e\). A singleton module \([M]\) has action represented by \(s\). For a longer word \(u\), an action \(A\otimes Eu\to Eu\) is represented on \([A]u\to u\) by composing it with \(\mu_{[A],u}^{-1}\). This last comparison is needed because the word is evaluated with fixed parentheses.

6. Four graded exercises with full solutions

Exercise 1 — A word model contains more than letterwise maps (introductory)

Over a field let \(V=k^2\), \(W=k^3\). Compare the words \(u=[V,W]\) and \(v=[V\otimes W]\) in \(\mathcal W\mathsf{Vect}_k\). Describe their Hom space and construct an invertible endomorphism of \(u\) that is not a single tensor product of two maps on the letters.

Solution. Both evaluations are \(V\otimes W\), so the identity representative gives an isomorphism \(u\to v\), although the words have different lengths. Their Hom space is the full space of linear maps \(k^6\to k^6\), of dimension \(36\) after bases are chosen. Put \(N_V(e_2)=e_1\), \(N_V(e_1)=0\), and \(N_W(f_2)=f_1\), \(N_W(f_1)=N_W(f_3)=0\). Then \[ \begin{gathered}T=1+N_V\otimes N_W,\\ T^{-1}=1-N_V\otimes N_W,\end{gathered} \] because the added map squares to zero. If \(T=p\otimes q\), the identity of \(T\) on \(e_1\otimes W\) forces \(p(e_1)=c e_1\) with \(c\ne0\), and \(q=c^{-1}1_W\). Its identity on \(e_2\otimes f_1\) then forces \(p(e_2)=c e_2\). This would make \(T\) the identity, contrary to its value \(e_2\otimes f_2+e_1\otimes f_1\) on \(e_2\otimes f_2\). Thus it is a genuine full-morphism word arrow absent from the letterwise free construction. \(\square\)

Exercise 2 — Noninvertible monoidal transformations (intermediate)

Let \(\mathcal C\) be the discrete strict monoidal category of nonnegative integers under addition. Let \(\mathsf{Mat}_k\) have dimensions as objects, matrices as arrows and Kronecker tensor; ordered indices make it strict. Take the strict functor \(F(n)=2^n\). Classify monoidal natural endomorphisms of \(F\), and extend one noninvertible example to \(\mathcal W\mathcal C\).

Solution. There are no nonidentity arrows imposing naturality equations. The empty tensor forces \(\alpha_0=1_k\), and \(n=1+\cdots+1\) forces \(\alpha_n=h^{\otimes n}\) for the matrix \(h=\alpha_1\). Conversely these matrices satisfy every tensor equation by associativity of Kronecker tensor, so every \(2\)-by-\(2\) matrix occurs. Choose \(h=\operatorname{diag}(1,0)\). For \(n>0\) the resulting matrix has rank one and is idempotent, hence noninvertible. On a word \((n_1,\ldots,n_r)\), its strict extension is \(h^{\otimes(n_1+\cdots+n_r)}\), with scalar identity for the empty word. The comparisons \(\phi\) are identity here, so (3.5) gives precisely this formula. Words with the same sum have the unique identity representative between their evaluations in \(\mathcal C\); the displayed components coincide on such words, verifying naturality for every word arrow. In particular the one-letter word \([0]\) and the empty word both have identity component, as required by their isomorphism. \(\square\)

Exercise 3 — The full module category survives (advanced)

Let \(A=k[\varepsilon]/(\varepsilon^2)\) and \(M=k^2\), with \(\varepsilon\) acting by \(N(e_2)=e_1\), \(N(e_1)=0\). Give the singleton-word algebra and module, write the action matrix, and compute every module endomorphism before and after strictification.

Solution. The algebra multiplication \([A,A]\to[A]\) sends \(1\otimes1\) to \(1\), \(1\otimes\varepsilon\) and \(\varepsilon\otimes1\) to \(\varepsilon\), and \(\varepsilon\otimes\varepsilon\) to zero. Its unit is the arrow \([]\to[A]\) represented by \(1\mapsto1\). The module action \([A,M]\to[M]\), on the ordered basis \(1\otimes e_1,1\otimes e_2,\varepsilon\otimes e_1,\varepsilon\otimes e_2\), is \[ \begin{pmatrix}1&0&0&1\\0&1&0&0\end{pmatrix}. \] Associativity reduces to \(N^2=0\), and the unit acts as identity. An endomorphism commutes with the action exactly when it commutes with \(N\). Multiplying two-by-two matrices gives all such maps as \[ \begin{pmatrix}a&b\\0&a\end{pmatrix}, \qquad a,b\in k. \] They are invertible exactly for \(a\ne0\). In the word model Hom sets are still the full underlying linear-map sets, and the represented action equation is the same equation. Thus the entire endomorphism algebra, including the noninvertible maps with \(a=0\), survives. This is an explicit check of Proposition 5.1 on a fixed algebra and its full module category. \(\square\)

Exercise 4 — A strict model need not erase an associator scalar (advanced)

Consider a monoidal groupoid with objects \(0,1\) under addition modulo two, automorphism group \(\{1,-1\}\) at each object, and no arrows between different objects. Tensor and composition multiply scalars. Units are strict, and the associator at \((g,h,k)\) is \((-1)^{ghk}\). Verify its axioms, show that an identity underlying functor with identity unit comparison cannot make it strict by a tensor comparison alone, and locate the sign in its word model.

Solution. Naturality holds because the scalar groups are commutative. All associators with a zero entry are identity, giving the triangle. In the pentagon the exponents modulo two are \[ \begin{gathered} hkl+g(h+k)l+ghk,\\ (g+h)kl+gh(k+l). \end{gathered} \] Expanding gives the same four terms, proving the pentagon. A tensor comparison for the identity underlying functor is a scalar \(c(g,h)\). Identity unit comparison forces \(c(0,g)=c(g,0)=1\). At \((1,1,1)\), the strong functor associativity equation would require \[ c(1,0)c(1,1) =-c(0,1)c(1,1), \] which is impossible in \(\{1,-1\}\). Thus this way of strictifying on the same underlying category fails. In the word model, however, objects are words and the associator is identity on the three-letter word. The evaluation comparison \(\mu_{[1,1],[1]}\) is identity by left association, whereas \(\mu_{[1],[1,1]}\) is the inverse original associator, namely \(-1\). Equation (1.3) retains that scalar exactly. Also the original endomorphism \(-1:1\to1\) remains a nonidentity singleton-word arrow by (2.1). Strictness of structural parentheses has therefore neither discarded an original arrow nor forced its scalar to be identity. \(\square\)

7. Further reading and licence

• Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych and Victor Ostrik, Tensor Categories, author-hosted final version, Sections 2.4, 2.8 and 2.9, for monoidal functors, strictness and coherence. Their strictness proof uses an endofunctor construction; the proof above uses a full-morphism word model and the independently normalized coherence prerequisite.
• Markus Himmel, Mathlib monoidal coherence, for the normalization proof used in Section 1, under its Apache 2.0 licence. Its discrete normal forms and natural normalization isomorphism prove equality of formal structural maps before any strictification is used here. No source code is reproduced in this lesson.

The exposition, constructions and four worked solutions are released under CC0-1.0. Linked works retain their own copyrights and licences.