nLab Day's reflection theorem



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


(Day) Let R:CDR: C \to D be a fully faithful functor with left adjoint L:DCL \colon D \to C, and suppose given a symmetric monoidal closed structure on DD with tensor \otimes and internal hom [,][-, -]. Then for objects cc of CC and d,dd, d' of DD, the following are equivalent:

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

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

  3. L(u1):L(dd)L(RLdd)L(u \otimes 1) \colon L(d \otimes d') \to L(R L d \otimes d') is an isomorphism;

  4. L(uu):L(dd)L(RLdRLd)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 RR is fully faithful, the monad RLR L is idempotent. Consequently, R:CDR: C \to D is monadic, and algebra structures on an object dd are unique when they exist. This makes algebra structure on dd a property, that dRcd \cong R c for some cc in CC, unique up to isomorphism. Call this property “being in CC”. Thus condition 1.\text{1.} says that [d,d][d, d'] is in CC for a particular dRcd' \cong R c in CC. (If DD is cartesian closed and [d,d]C[d, d'] \in C whenever dDd' \in D, we say CC is an exponential ideal in DD.) Notice that all DD-maps between objects in CC are algebra maps, by full faithfulness of RR.

  • (b) If dd is in CC, then for any dd' the unit u:dRLdu\colon d' \to R L d' induces an isomorphism D(RLd,d)D(d,d)D(R L d', d) \cong D(d', d), since every fD(RLd,d)f \in D(R L d', d) is an algebra map RLddR L d' \to d and RLdR L d' is the free algebra on dd'.


We prove\text{3.} \Rightarrow \text{4.} \Rightarrow \text{1.}\; \Rightarrow\; \text{3.}, and then 2.3.\text{2.} \Leftrightarrow \text{3.}. Some parts are merely sketched; refer to Day for full details.

3.4.\text{3.}\; \Rightarrow\; \text{4.} is obvious from the symmetric structure and

4.1.\text{4.} \Rightarrow \text{1.} is proven by giving an algebra structure RL[d,Rc][d,Rc]R L[d, R c] \to [d, R c], obtained by currying the following composite:

(by idempotence of RLR L, to prove this map is an algebra structure, it suffices to show it is left inverse to the unit).

1.3.\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)D(1, u) are isomorphisms by assuming 1.\text{1.}, and the bottom map labeled D(u,1)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 cc of CC, the map L(u1)L(u \otimes 1) is an isomorphism by the Yoneda lemma, so that 4.\text{4.} holds.

Finally, 2.3.\text{2.} \Leftrightarrow \text{3.} is proven by considering the diagram

and again applying a Yoneda lemma argument.



If LL is a strong symmetric monoidal functor, then for any cc in CC and dd in DD, the internal hom [d,c][d, c] is in CC.


Full faithfulness of RR is equivalent to the counit ε:LR1 C\varepsilon \colon L R \to 1_C being an isomorphism. By a triangle identity, this forces LuL u to be an isomorphism for any unit u:dRLdu: d \to R L d. This in turn forces the arrow L(uu)L(u \otimes u) in the diagram

to be an isomorphism, where the vertical arrows are invertible symmetry constraints and the maps LuL u are isomorphisms. Now apply the equivalence between 4.\text{4.} and 1.\text{1.} from the reflection theorem.


If DD is cartesian closed, and the reflector L:DCL \colon D \to C preserves products, then CC is cartesian closed.


We have already seen under the hypotheses that if c,cc, c' are in CC, then the exponential c cc^{c'} as calculated in DD is in CC. Furthermore, CC inherits products from DD, because R:CDR \colon C \to D is monadic and monadic functors reflect limits. The adjunction C(c×c,c)C(c,c c)C(c'' \times c', c) \cong C(c'', c^{c'}) holds because it holds when interpreted in DD and CC is fully embedded in DD.


Last revised on May 28, 2023 at 23:26:12. See the history of this page for a list of all contributions to it.