mathlib docs: category_theory.adjunction.reflective

@[class]

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

to_is_right_adjoint : category_theory.is_right_adjoint R
to_full : category_theory.full R
to_faithful : category_theory.faithful R

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

Instances

source

theorem category_theory.unit_obj_eq_map_unit {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] (X : C) :

(category_theory.adjunction.of_right_adjoint i).unit.app (i.obj ((category_theory.left_adjoint i).obj X)) = i.map ((category_theory.left_adjoint i).map ((category_theory.adjunction.of_right_adjoint i).unit.app X))

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

source

@[instance]

def category_theory.is_iso_unit_obj {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] {B : D} :

category_theory.is_iso ((category_theory.adjunction.of_right_adjoint i).unit.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.ess_image.unit_iso.

Equations

category_theory.is_iso_unit_obj = category_theory.is_iso_unit_obj._proof_1.mpr category_theory.is_iso.inv_is_iso

source

def category_theory.functor.ess_image.unit_is_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] {A : C} (h : A ∈ i.ess_image) :

category_theory.is_iso ((category_theory.adjunction.of_right_adjoint i).unit.app A)

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