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
.
- 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 of this typeclass
- category_theory.reflective.comp
- category_theory.mono_over.reflective
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.reflective
- algebraic_geometry.Spec.reflective
- CompHaus_to_Top.reflective
- Profinite.to_CompHaus.reflective
- Profinite.to_Top.reflective
- UniformSpace.category_theory.forget₂.category_theory.reflective
Instances of other typeclasses for category_theory.reflective
- category_theory.reflective.has_sizeof_inst
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.
Equations
(Implementation) Auxiliary definition for unit_comp_partial_bijective
.
The description of the inverse of the bijection unit_comp_partial_bijective_aux
.
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.
Equations
- category_theory.unit_comp_partial_bijective A hB = (((category_theory.iso.refl A).hom_congr (category_theory.functor.ess_image.get_iso hB).symm).trans (category_theory.unit_comp_partial_bijective_aux A (category_theory.functor.ess_image.witness hB))).trans ((category_theory.iso.refl (i.obj ((category_theory.left_adjoint i).obj A))).hom_congr (category_theory.functor.ess_image.get_iso hB))
If i : D ⥤ C
is reflective, the inverse functor of i ≌ F.ess_image
can be explicitly
defined by the reflector.
Equations
- category_theory.equiv_ess_image_of_reflective = {functor := i.to_ess_image, inverse := i.ess_image_inclusion ⋙ category_theory.left_adjoint i, unit_iso := category_theory.nat_iso.of_components (λ (X : D), (category_theory.as_iso ((category_theory.adjunction.of_right_adjoint i).counit.app X)).symm) category_theory.equiv_ess_image_of_reflective._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (X : i.ess_image_subcategory), (category_theory.as_iso ((category_theory.adjunction.of_right_adjoint i).unit.app X.obj)).symm) category_theory.equiv_ess_image_of_reflective._proof_4, functor_unit_iso_comp' := _}