nLab Day's reflection theorem

Idea

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.

Statement and Proof

Theorem

(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:

1. $u[d, R c] \colon [d, R c] \to R L[d, R c]$ is an isomorphism;

2. $[u, 1] \colon [R L d, R c] \to [d, R c]$ is an isomorphism;

3. $L(u \otimes 1) \colon L(d \otimes d') \to L(R L d \otimes d')$ is an isomorphism;

4. $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'$.

Proof

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.

Consequences

Corollary

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$.

Proof

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.

Corollary

If $D$ is cartesian closed, and the reflector $L \colon D \to C$ preserves products, then $C$ is cartesian closed.

Proof

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$.

Reference

• Brian Day, A reflection theorem for closed categories, Journal of Pure and Applied Algebra 2 1 (1972), 1-11. [doi:10.1016/0022-4049(72)90021-7]