Cotensoring commutative monoids by finite sets

Proof. For a finite set \(S\) and a commutative monoid \(X\) we define the cotensoring by \(X^S(T) := X(S \times T)\) for \(T \in \Fin \). The functoriality in \(S\) and \(T\) comes from the observation that the product functor \(- \times -\colon \Fin \times \Fin \to \Fin \) induces a functor on span categories by taking products of spans: \[ - \times - \colon \Span (\Fin ) \times \Span (\Fin ) \to \Span (\Fin ), \qquad (S, T) \mapsto S \times T. \] (This is no longer the categorical product in \(\Span (\Fin )\)!)

• Since we have a natural bijection \(* \times T \cong T\), it is clear that the cotensoring is the identity on \(\{*\} \times \CMon (C)\).
• Fixing \(S \in \Fin \), the functor \((-)^S\colon \CMon (C) \to \CMon (C)\) preserves finite products: we may check this pointwise for every \(T \in \Fin \), where it is by definition given by the evaluation \(X \mapsto X(S \times T)\), which preserves finite products.
• Fixing \(X \in \CMon (C)\), the functor \(X^{(-)}\colon \Span (\Fin ) \to \CMon (C)\) preserves finite products: again we may check this pointwise for every \(T \in \Fin \), where we may write it as the composite \[ \Span (\Fin ) \xrightarrow {- \times T} \Span (\Fin ) \xrightarrow {X} C. \] But \(X\) preserves finite products by assumption and \(- \times T\) preserves finite products since the functor \(- \times T\colon \Fin \to \Fin \) preserves finite coproducts: \(\bigsqcup _{i=1}^n (S_i \times T) \iso (\bigsqcup _{i=1}^n S_i) \times T\).

In particular we see that \(X^S\) is the \(S\)-fold product of \(X\) in \(\CMon (C)\), explaining the notation. □