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 CategoryTheory.Monad.Limits.

class CategoryTheory.Reflective {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) extends CategoryTheory.IsRightAdjoint , CategoryTheory.Functor.Full , CategoryTheory.Functor.Faithful : Type (max (max (max u₁ u₂) v₁) v₂)

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

theorem CategoryTheory.unit_obj_eq_map_unit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : C) : (CategoryTheory.Adjunction.ofRightAdjoint i).unit.app (i.obj ((CategoryTheory.leftAdjoint i).obj X)) = i.map ((CategoryTheory.leftAdjoint i).map ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app X))

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

theorem CategoryTheory.Functor.essImage.unit_isIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] {A : C} (h : A ∈ CategoryTheory.Functor.essImage i) : CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint 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.)

theorem CategoryTheory.mem_essImage_of_unit_isIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint i] (A : C) [CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A)] : A ∈ CategoryTheory.Functor.essImage i

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

theorem CategoryTheory.mem_essImage_of_unit_isSplitMono {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] {A : C} [CategoryTheory.IsSplitMono ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A)] : A ∈ CategoryTheory.Functor.essImage i

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

instance CategoryTheory.Reflective.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Reflective F] [CategoryTheory.Reflective G] : CategoryTheory.Reflective (CategoryTheory.Functor.comp F G)

Composition of reflective functors.

Equations

• CategoryTheory.Reflective.comp F G = CategoryTheory.Reflective.mk

def CategoryTheory.unitCompPartialBijectiveAux {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) (B : D) : (A ⟶ i.obj B) ≃ (i.obj ((CategoryTheory.leftAdjoint i).obj A) ⟶ i.obj B)

(Implementation) Auxiliary definition for unitCompPartialBijective.

Equations

• CategoryTheory.unitCompPartialBijectiveAux A B = ((CategoryTheory.Adjunction.ofRightAdjoint i).homEquiv A B).symm.trans (CategoryTheory.equivOfFullyFaithful i)

theorem CategoryTheory.unitCompPartialBijectiveAux_symm_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] {A : C} {B : D} (f : i.obj ((CategoryTheory.leftAdjoint i).obj A) ⟶ i.obj B) : (CategoryTheory.unitCompPartialBijectiveAux A B).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A) f

The description of the inverse of the bijection unitCompPartialBijectiveAux.

def CategoryTheory.unitCompPartialBijective {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B : C} (hB : B ∈ CategoryTheory.Functor.essImage i) : (A ⟶ B) ≃ (i.obj ((CategoryTheory.leftAdjoint 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 fun (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 unitCompPartialBijective_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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.unitCompPartialBijective_symm_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B : C} (hB : B ∈ CategoryTheory.Functor.essImage i) (f : i.obj ((CategoryTheory.leftAdjoint i).obj A) ⟶ B) : (CategoryTheory.unitCompPartialBijective A hB).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A) f

theorem CategoryTheory.unitCompPartialBijective_symm_natural {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B : C} {B' : C} (h : B ⟶ B') (hB : B ∈ CategoryTheory.Functor.essImage i) (hB' : B' ∈ CategoryTheory.Functor.essImage i) (f : i.obj ((CategoryTheory.leftAdjoint i).obj A) ⟶ B) : (CategoryTheory.unitCompPartialBijective A hB').symm (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB).symm f) h

theorem CategoryTheory.unitCompPartialBijective_natural {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B : C} {B' : C} (h : B ⟶ B') (hB : B ∈ CategoryTheory.Functor.essImage i) (hB' : B' ∈ CategoryTheory.Functor.essImage i) (f : A ⟶ B) : (CategoryTheory.unitCompPartialBijective A hB') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB) f) h

instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToPrefunctorIdObjEssImageCompLeftAdjointToIsRightAdjointAppUnitOfRightAdjoint {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : CategoryTheory.Functor.EssImageSubcategory i) : CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app X.obj)

Equations

• ⋯ = ⋯

def CategoryTheory.equivEssImageOfReflective_counitIso_app {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : CategoryTheory.Functor.EssImageSubcategory i) : (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp (CategoryTheory.Functor.essImageInclusion i) (CategoryTheory.leftAdjoint i)) (CategoryTheory.Functor.toEssImage i)).obj X ≅ X

The counit isomorphism of the equivalence D ≌ i.EssImageSubcategory given by equivEssImageOfReflective when the functor i is reflective.

Equations

• CategoryTheory.equivEssImageOfReflective_counitIso_app X = (CategoryTheory.asIso ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app X.obj)).symm

theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_hom {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : CategoryTheory.Functor.EssImageSubcategory i) : (CategoryTheory.Functor.essImageInclusion i).map (CategoryTheory.equivEssImageOfReflective_counitIso_app X).hom = CategoryTheory.inv ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app X.obj)

theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_inv {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : CategoryTheory.Functor.EssImageSubcategory i) : (CategoryTheory.Functor.essImageInclusion i).map (CategoryTheory.equivEssImageOfReflective_counitIso_app X).inv = (CategoryTheory.Adjunction.ofRightAdjoint i).unit.app X.obj

@[simp]

theorem CategoryTheory.equivEssImageOfReflective_unitIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : D) => (CategoryTheory.asIso ((CategoryTheory.Adjunction.ofRightAdjoint i).counit.app X)).symm) ⋯

@[simp]

theorem CategoryTheory.equivEssImageOfReflective_counitIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.equivEssImageOfReflective_counitIso_app ⋯

@[simp]

theorem CategoryTheory.equivEssImageOfReflective_functor {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.functor = CategoryTheory.Functor.toEssImage i

@[simp]

theorem CategoryTheory.equivEssImageOfReflective_inverse {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.inverse = CategoryTheory.Functor.comp (CategoryTheory.Functor.essImageInclusion i) (CategoryTheory.leftAdjoint i)

def CategoryTheory.equivEssImageOfReflective {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : D ≌ CategoryTheory.Functor.EssImageSubcategory i

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

Equations

• One or more equations did not get rendered due to their size.