# 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 category_theory.monad.limits.

@[class]
structure category_theory.reflective {C : Type u₁} {D : Type u₂} (R : D C) :
Type (max u₁ u₂ v₁ v₂)
• to_full :
• to_faithful :

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

Instances
theorem category_theory.unit_obj_eq_map_unit {C : Type u₁} {D : Type u₂} {i : D C} (X : C) :

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

@[instance]
def category_theory.is_iso_unit_obj {C : Type u₁} {D : Type u₂} {i : D C} {B : D} :

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.ess_image.unit_iso.

Equations
def category_theory.functor.ess_image.unit_is_iso {C : Type u₁} {D : Type u₂} {i : D C} {A : C} (h : A i.ess_image) :

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

Equations
theorem category_theory.mem_ess_image_of_unit_is_iso {C : Type u₁} {D : Type u₂} {i : D C} (A : C)  :

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

theorem category_theory.mem_ess_image_of_unit_split_mono {C : Type u₁} {D : Type u₂} {i : D C} {A : C}  :

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

@[instance]
def category_theory.reflective.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E) [Fr : category_theory.reflective F] [Gr : category_theory.reflective G] :

Composition of reflective functors.

Equations