Day's reflection theorem

Let D be a symmetric monoidal closed category and let C be a reflective subcategory. Day's reflection theorem proves the equivalence of four conditions, which are all of the form that a map obtained by acting on the unit of the reflective adjunction, with the internal hom and tensor functors, is an isomorphism.

Suppose that C is itself monoidal and that the reflector is a monoidal functor. Then we can apply Day's reflection theorem to prove that C is also closed monoidal.

References

• We follow the proof on nLab, see https://ncatlab.org/nlab/show/Day%27s+reflection+theorem.
• The original paper is [Day72] A reflection theorem for closed categories, by Day, 1972.

theorem CategoryTheory.Monoidal.Reflective.isIso_tfae {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.MonoidalClosed D] {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] {L : CategoryTheory.Functor D C} (adj : L ⊣ R) : [∀ (c : C) (d : D), CategoryTheory.IsIso (adj.unit.app ((CategoryTheory.ihom d).obj (R.obj c))), ∀ (c : C) (d : D), CategoryTheory.IsIso ((CategoryTheory.MonoidalClosed.pre (adj.unit.app d)).app (R.obj c)), ∀ (d d' : D), CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategory.whiskerRight (adj.unit.app d) d')), ∀ (d d' : D), CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategory.tensorHom (adj.unit.app d) (adj.unit.app d')))].TFAE

Day's reflection theorem.

Let D be a symmetric monoidal closed category and let C be a reflective subcategory. Denote by R : C ⥤ D the inclusion functor and by L : D ⥤ C the reflector. Let u denote the unit of the adjunction L ⊣ R. Denote the internal hom by [-,-]. The following are equivalent:

1. u : [d, Rc] ⟶ RL[d, Rc] is an isomorphism,
2. [u, 𝟙] : [RLd, Rc] ⟶ [d, Rc] is an isomorphism,
3. L(u ▷ d') : L(d ⊗ d') ⟶ L(RLd ⊗ d') is an isomorphism,
4. L(u ⊗ u) : L(d ⊗ d') ⟶ L(RLd ⊗ RLd') is an isomorphism,

where c, d, d' are arbitrary objects of C/D, quantified over separately in each condition.

instance CategoryTheory.Monoidal.Reflective.instIsIsoMapTensorHomAppUnit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Functor D C} [L.Monoidal] {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] (adj : L ⊣ R) (d d' : D) : CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategory.tensorHom (adj.unit.app d) (adj.unit.app d')))

Equations

• ⋯ = ⋯

instance CategoryTheory.Monoidal.Reflective.instIsIsoAppUnitObjIhom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.MonoidalClosed D] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Functor D C} [L.Monoidal] {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] (adj : L ⊣ R) (c : C) (d : D) : CategoryTheory.IsIso (adj.unit.app ((CategoryTheory.ihom d).obj (R.obj c)))

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Monoidal.Reflective.closed {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.MonoidalClosed D] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Functor D C} [L.Monoidal] {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] (adj : L ⊣ R) (c : C) : CategoryTheory.Closed c

Auxiliary definition for monoidalClosed.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Monoidal.Reflective.monoidalClosed {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.MonoidalClosed D] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Functor D C} [L.Monoidal] {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] (adj : L ⊣ R) : CategoryTheory.MonoidalClosed C

Given a reflective functor R : C ⥤ D with a monoidal left adjoint, such that D is symmetric monoidal closed, then C is monoidal closed.

Equations

• CategoryTheory.Monoidal.Reflective.monoidalClosed adj = { closed := fun (c : C) => CategoryTheory.Monoidal.Reflective.closed adj c }