# Reflective functors #

Basic properties of reflective functors, especially those relating to their essential image.

Note properties of reflective functors relating to limits and colimits are included in CategoryTheory.Monad.Limits.

class CategoryTheory.Reflective {C : Type u₁} {D : Type u₂} [] [] (R : ) extends , , :
Type (max (max (max u₁ u₂) v₁) v₂)

A functor is reflective, or a reflective inclusion, if it is fully faithful and right adjoint.

Instances
theorem CategoryTheory.unit_obj_eq_map_unit {C : Type u₁} {D : Type u₂} [] [] {i : } (X : C) :
.app (i.obj (().obj X)) = i.map (().map (.app X))

For a reflective functor i (with left adjoint L), with unit η, we have η_iL = iL η.

instance CategoryTheory.isIso_unit_obj {C : Type u₁} {D : Type u₂} [] [] {i : } {B : D} :
CategoryTheory.IsIso (.app (i.obj B))

When restricted to objects in D given by i : D ⥤ C, the unit is an isomorphism. In other words, η_iX is an isomorphism for any X in D. More generally this applies to objects essentially in the reflective subcategory, see Functor.essImage.unit_isIso.

theorem CategoryTheory.Functor.essImage.unit_isIso {C : Type u₁} {D : Type u₂} [] [] {i : } {A : C} (h : ) :

If A is essentially in the image of a reflective functor i, then η_A is an isomorphism. This gives that the "witness" for A being in the essential image can instead be given as the reflection of A, with the isomorphism as η_A.

(For any B in the reflective subcategory, we automatically have that ε_B is an iso.)

theorem CategoryTheory.mem_essImage_of_unit_isIso {C : Type u₁} {D : Type u₂} [] [] {i : } (A : C) [CategoryTheory.IsIso (.app A)] :

If η_A is an isomorphism, then A is in the essential image of i.

theorem CategoryTheory.mem_essImage_of_unit_isSplitMono {C : Type u₁} {D : Type u₂} [] [] {i : } {A : C} [CategoryTheory.IsSplitMono (.app A)] :

If η_A is a split monomorphism, then A is in the reflective subcategory.

instance CategoryTheory.Reflective.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [] [] [] (F : ) (G : ) :

Composition of reflective functors.

def CategoryTheory.unitCompPartialBijectiveAux {C : Type u₁} {D : Type u₂} [] [] {i : } (A : C) (B : D) :
(A i.obj B) (i.obj (().obj A) i.obj B)

(Implementation) Auxiliary definition for unitCompPartialBijective.

Instances For
theorem CategoryTheory.unitCompPartialBijectiveAux_symm_apply {C : Type u₁} {D : Type u₂} [] [] {i : } {A : C} {B : D} (f : i.obj (().obj A) i.obj B) :
().symm f =

The description of the inverse of the bijection unitCompPartialBijectiveAux.

def CategoryTheory.unitCompPartialBijective {C : Type u₁} {D : Type u₂} [] [] {i : } (A : C) {B : C} (hB : ) :
(A B) (i.obj (().obj A) B)

If i has a reflector L, then the function (i.obj (L.obj A) ⟶ B) → (A ⟶ B) given by precomposing with η.app A is a bijection provided B is in the essential image of i. That is, the function λ (f : i.obj (L.obj A) ⟶ B), η.app A ≫ f is bijective, as long as B is in the essential image of i. This definition gives an equivalence: the key property that the inverse can be described nicely is shown in unitCompPartialBijective_symm_apply.

This establishes there is a natural bijection (A ⟶ B) ≃ (i.obj (L.obj A) ⟶ B). In other words, from the point of view of objects in D, A and i.obj (L.obj A) look the same: specifically that η.app A is an isomorphism.

Instances For
@[simp]
theorem CategoryTheory.unitCompPartialBijective_symm_apply {C : Type u₁} {D : Type u₂} [] [] {i : } (A : C) {B : C} (hB : ) (f : i.obj (().obj A) B) :
().symm f =
theorem CategoryTheory.unitCompPartialBijective_symm_natural {C : Type u₁} {D : Type u₂} [] [] {i : } (A : C) {B : C} {B' : C} (h : B B') (hB : ) (hB' : ) (f : i.obj (().obj A) B) :
().symm () =
theorem CategoryTheory.unitCompPartialBijective_natural {C : Type u₁} {D : Type u₂} [] [] {i : } (A : C) {B : C} {B' : C} (h : B B') (hB : ) (hB' : ) (f : A B) :
def CategoryTheory.equivEssImageOfReflective_counitIso_app {C : Type u₁} {D : Type u₂} [] [] {i : } :
().obj X X

The counit isomorphism of the equivalence D ≌ i.EssImageSubcategory given by equivEssImageOfReflective when the functor i is reflective.

Instances For
theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_inv {C : Type u₁} {D : Type u₂} [] [] {i : } :
= .app X.obj
@[simp]
theorem CategoryTheory.equivEssImageOfReflective_inverse {C : Type u₁} {D : Type u₂} [] [] {i : } :
CategoryTheory.equivEssImageOfReflective.inverse =
@[simp]
theorem CategoryTheory.equivEssImageOfReflective_functor {C : Type u₁} {D : Type u₂} [] [] {i : } :
CategoryTheory.equivEssImageOfReflective.functor =
@[simp]
theorem CategoryTheory.equivEssImageOfReflective_unitIso {C : Type u₁} {D : Type u₂} [] [] {i : } :
CategoryTheory.equivEssImageOfReflective.unitIso = CategoryTheory.NatIso.ofComponents fun X => (CategoryTheory.asIso (().counit.app X)).symm
@[simp]
theorem CategoryTheory.equivEssImageOfReflective_counitIso {C : Type u₁} {D : Type u₂} [] [] {i : } :
CategoryTheory.equivEssImageOfReflective.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.equivEssImageOfReflective_counitIso_app
def CategoryTheory.equivEssImageOfReflective {C : Type u₁} {D : Type u₂} [] [] {i : } :

If i : D ⥤ C is reflective, the inverse functor of i ≌ F.essImage can be explicitly defined by the reflector.

Instances For