Theorems · Theorem · category theory

CategoryTheory.Monoidal.Reflective.isIso_tfae

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  [CategoryTheory.SymmetricCategory D] [inst_4 : 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 (d ⟹ 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.MonoidalCategoryStruct.whiskerRight (adj.unit.app d) d')),
      ∀ (d d' : D),
        CategoryTheory.IsIso
          (L.map (CategoryTheory.MonoidalCategoryStruct.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.

Defined in

Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Cited by

0 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.SymmetricCategoryCategoryTheory.MonoidalClosedCategoryTheory.Functor.FaithfulCategoryTheory.Functor.Full