Day’s reflection theorem [Day (1972)] gives conditions under which a reflective subcategory of a symmetric monoidal closed category is closed under internal homs.
One memorable consequence of the theorem is that the subcategory is closed under internal homs if the reflector is symmetric strong monoidal.
(Day) Let $R: C \to D$ be a fully faithful functor with left adjoint $L \colon D \to C$, and suppose given a symmetric monoidal closed structure on $D$ with tensor $\otimes$ and internal hom $[-, -]$. Then for objects $c$ of $C$ and $d, d'$ of $D$, the following are equivalent:
$u[d, R c] \colon [d, R c] \to R L[d, R c]$ is an isomorphism;
$[u, 1] \colon [R L d, R c] \to [d, R c]$ is an isomorphism;
$L(u \otimes 1) \colon L(d \otimes d') \to L(R L d \otimes d')$ is an isomorphism;
$L(u \otimes u) \colon L(d \otimes d') \to L(R L d \otimes R L d')$ is an isomorphism.
Some remarks before the proof:
(a) Since $R$ is fully faithful, the monad $R L$ is idempotent. Consequently, $R: C \to D$ is monadic, and algebra structures on an object $d$ are unique when they exist. This makes algebra structure on $d$ a property, that $d \cong R c$ for some $c$ in $C$, unique up to isomorphism. Call this property “being in $C$”. Thus condition $\text{1.}$ says that $[d, d']$ is in $C$ for a particular $d' \cong R c$ in $C$. (If $D$ is cartesian closed and $[d, d'] \in C$ whenever $d' \in D$, we say $C$ is an exponential ideal in $D$.) Notice that all $D$-maps between objects in $C$ are algebra maps, by full faithfulness of $R$.
(b) If $d$ is in $C$, then for any $d'$ the unit $u\colon d' \to R L d'$ induces an isomorphism $D(R L d', d) \cong D(d', d)$, since every $f \in D(R L d', d)$ is an algebra map $R L d' \to d$ and $R L d'$ is the free algebra on $d'$.
We prove $\text{3.} \Rightarrow \text{4.} \Rightarrow \text{1.}\; \Rightarrow\; \text{3.}$, and then $\text{2.} \Leftrightarrow \text{3.}$. Some parts are merely sketched; refer to Day for full details.
$\text{3.}\; \Rightarrow\; \text{4.}$ is obvious from the symmetric structure and
$\text{4.} \Rightarrow \text{1.}$ is proven by giving an algebra structure $R L[d, R c] \to [d, R c]$, obtained by currying the following composite:
(by idempotence of $R L$, to prove this map is an algebra structure, it suffices to show it is left inverse to the unit).
$\text{1.} \Rightarrow \text{3.}$ is proven by considering the diagram
which commutes by functoriality and naturality, and where the maps labeled $D(1, u)$ are isomorphisms by assuming $\text{1.}$, and the bottom map labeled $D(u, 1)$ is an isomorphism by invoking remark (b). It follows that the top horizontal map is also an isomorphism. Since this holds for all objects $c$ of $C$, the map $L(u \otimes 1)$ is an isomorphism by the Yoneda lemma, so that $\text{4.}$ holds.
Finally, $\text{2.} \Leftrightarrow \text{3.}$ is proven by considering the diagram
and again applying a Yoneda lemma argument.
If $L$ is a strong symmetric monoidal functor, then for any $c$ in $C$ and $d$ in $D$, the internal hom $[d, c]$ is in $C$.
Full faithfulness of $R$ is equivalent to the counit $\varepsilon \colon L R \to 1_C$ being an isomorphism. By a triangle identity, this forces $L u$ to be an isomorphism for any unit $u: d \to R L d$. This in turn forces the arrow $L(u \otimes u)$ in the diagram
to be an isomorphism, where the vertical arrows are invertible symmetry constraints and the maps $L u$ are isomorphisms. Now apply the equivalence between $\text{4.}$ and $\text{1.}$ from the reflection theorem.
If $D$ is cartesian closed, and the reflector $L \colon D \to C$ preserves products, then $C$ is cartesian closed.
We have already seen under the hypotheses that if $c, c'$ are in $C$, then the exponential $c^{c'}$ as calculated in $D$ is in $C$. Furthermore, $C$ inherits products from $D$, because $R \colon C \to D$ is monadic and monadic functors reflect limits. The adjunction $C(c'' \times c', c) \cong C(c'', c^{c'})$ holds because it holds when interpreted in $D$ and $C$ is fully embedded in $D$.
Last revised on May 28, 2023 at 23:26:12. See the history of this page for a list of all contributions to it.