mathlib documentation


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.

structure category_theory.reflective {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (R : D C) :
Type (max u₁ u₂ v₁ v₂)

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


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


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.

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

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

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


Composition of reflective functors.


(Implementation) Auxiliary definition for unit_comp_partial_bijective.


The description of the inverse of the bijection unit_comp_partial_bijective_aux.

def category_theory.unit_comp_partial_bijective {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D C} [category_theory.reflective i] (A : C) {B : C} (hB : B i.ess_image) :

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