mathlib documentation

category_theory.adjunction.reflective

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.

source
@[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₂)

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

Instances of this typeclass
Instances of other typeclasses for category_theory.reflective
  • category_theory.reflective.has_sizeof_inst
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
@[protected, 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.

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

source
theorem category_theory.mem_ess_image_of_unit_is_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.is_right_adjoint i] (A : C) [category_theory.is_iso ((category_theory.adjunction.of_right_adjoint i).unit.app A)] :
A ∈ i.ess_image

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

source
theorem category_theory.mem_ess_image_of_unit_split_mono {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] {A : C} [category_theory.split_mono ((category_theory.adjunction.of_right_adjoint i).unit.app A)] :
A ∈ i.ess_image

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

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

Composition of reflective functors.

Equations
source
def category_theory.unit_comp_partial_bijective_aux {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] (A : C) (B : D) :
(A ⟶ i.obj B) ≃ (i.obj ((category_theory.left_adjoint i).obj A) ⟶ i.obj B)

(Implementation) Auxiliary definition for unit_comp_partial_bijective.

Equations
source
theorem category_theory.unit_comp_partial_bijective_aux_symm_apply {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] {A : C} {B : D} (f : i.obj ((category_theory.left_adjoint i).obj A) ⟶ i.obj B) :
⇑((category_theory.unit_comp_partial_bijective_aux A B).symm) f = (category_theory.adjunction.of_right_adjoint i).unit.app A ≫ f

The description of the inverse of the bijection unit_comp_partial_bijective_aux.

source
noncomputable 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) :
(A ⟶ B) ≃ (i.obj ((category_theory.left_adjoint i).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 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
source
@[simp]
theorem category_theory.unit_comp_partial_bijective_symm_apply {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) (f : i.obj ((category_theory.left_adjoint i).obj A) ⟶ B) :
⇑((category_theory.unit_comp_partial_bijective A hB).symm) f = (category_theory.adjunction.of_right_adjoint i).unit.app A ≫ f
source
theorem category_theory.unit_comp_partial_bijective_symm_natural {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] (A : C) {B B' : C} (h : B ⟶ B') (hB : B ∈ i.ess_image) (hB' : B' ∈ i.ess_image) (f : i.obj ((category_theory.left_adjoint i).obj A) ⟶ B) :
⇑((category_theory.unit_comp_partial_bijective A hB').symm) (f ≫ h) = ⇑((category_theory.unit_comp_partial_bijective A hB).symm) f ≫ h
source
theorem category_theory.unit_comp_partial_bijective_natural {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] (A : C) {B B' : C} (h : B ⟶ B') (hB : B ∈ i.ess_image) (hB' : B' ∈ i.ess_image) (f : A ⟶ B) :
⇑(category_theory.unit_comp_partial_bijective A hB') (f ≫ h) = ⇑(category_theory.unit_comp_partial_bijective A hB) f ≫ h
source
@[simp]
theorem category_theory.equiv_ess_image_of_reflective_functor {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] :
category_theory.equiv_ess_image_of_reflective.functor = i.to_ess_image
source
@[simp]
theorem category_theory.equiv_ess_image_of_reflective_unit_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] :
category_theory.equiv_ess_image_of_reflective.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
source
@[simp]
theorem category_theory.equiv_ess_image_of_reflective_counit_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] :
category_theory.equiv_ess_image_of_reflective.counit_iso = category_theory.nat_iso.of_components (λ (X : ↥(i.ess_image)), (category_theory.as_iso ((category_theory.adjunction.of_right_adjoint i).unit.app ↑X)).symm) category_theory.equiv_ess_image_of_reflective._proof_4
source
@[simp]
theorem category_theory.equiv_ess_image_of_reflective_inverse {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] :
category_theory.equiv_ess_image_of_reflective.inverse = i.ess_image_inclusion ⋙ category_theory.left_adjoint i
source
noncomputable def category_theory.equiv_ess_image_of_reflective {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {i : D ⥤ C} [category_theory.reflective i] :
D ≌ ↥(i.ess_image)

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

Equations