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

class CategoryTheory.Reflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (R : Functor D C) extends R.Full, R.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.

• map_surjective {X Y : D} : Function.Surjective R.map
• map_injective {X Y : D} : Function.Injective R.map
• L : Functor C D

  a choice of a left adjoint to R

• adj : L R ⊣ R

  R is a right adjoint

def CategoryTheory.reflector {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (i : Functor D C) [Reflective i] : Functor C D

The reflector C ⥤ D when R : D ⥤ C is reflective.

def CategoryTheory.reflectorAdjunction {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (i : Functor D C) [Reflective i] : reflector i ⊣ i

The adjunction reflector i ⊣ i when i is reflective.

instance CategoryTheory.instIsRightAdjointOfReflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (i : Functor D C) [Reflective i] : i.IsRightAdjoint

instance CategoryTheory.instIsLeftAdjointReflector {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (i : Functor D C) [Reflective i] : (reflector i).IsLeftAdjoint

noncomputable def CategoryTheory.Functor.fullyFaithfulOfReflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (i : Functor D C) [Reflective i] : i.FullyFaithful

A reflective functor is fully faithful.

theorem CategoryTheory.unit_obj_eq_map_unit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (i : Functor D C) [Reflective i] (X : C) : (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) = i.map ((reflector i).map ((reflectorAdjunction 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₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {i : Functor D C} [Reflective i] {A : C} (h : i.essImage A) : IsIso ((reflectorAdjunction 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_isSplitMono {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {i : Functor D C} [Reflective i] {A : C} [IsSplitMono ((reflectorAdjunction i).unit.app A)] : i.essImage A

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

@[implicit_reducible]

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

Composition of reflective functors.

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

(Implementation) Auxiliary definition for unitCompPartialBijective.

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

The description of the inverse of the bijection unitCompPartialBijectiveAux.

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

@[simp]

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

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

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

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

theorem CategoryTheory.Functor.essImage_ext_iff {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {X Y : F.EssImageSubcategory} {f g : X ⟶ Y} : f = g ↔ F.essImage.ι.map f = F.essImage.ι.map g

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.equivEssImageOfReflective_counitIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {i : Functor D C} [Reflective i] : equivEssImageOfReflective.counitIso = Functor.fullyFaithfulCancelRight i.essImage.ι (NatIso.ofComponents (fun (X : i.EssImageSubcategory) => (asIso ((reflectorAdjunction i).unit.app X.obj)).symm) ⋯)

@[simp]

theorem CategoryTheory.equivEssImageOfReflective_unitIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {i : Functor D C} [Reflective i] : equivEssImageOfReflective.unitIso = (asIso (reflectorAdjunction i).counit).symm

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

A functor is coreflective, or a coreflective inclusion, if it is fully faithful and left adjoint.

• map_surjective {X Y : C} : Function.Surjective L.map
• map_injective {X Y : C} : Function.Injective L.map
• R : Functor D C

  a choice of a right adjoint to L

• adj : L ⊣ R L

  L is a left adjoint

def CategoryTheory.coreflector {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (j : Functor C D) [Coreflective j] : Functor D C

The coreflector D ⥤ C when L : C ⥤ D is coreflective.

def CategoryTheory.coreflectorAdjunction {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (j : Functor C D) [Coreflective j] : j ⊣ coreflector j

The adjunction j ⊣ coreflector j when j is coreflective.

instance CategoryTheory.instIsLeftAdjointOfCoreflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (j : Functor C D) [Coreflective j] : j.IsLeftAdjoint

instance CategoryTheory.instIsRightAdjointCoreflector {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (j : Functor C D) [Coreflective j] : (coreflector j).IsRightAdjoint

noncomputable def CategoryTheory.Functor.fullyFaithfulOfCoreflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (j : Functor C D) [Coreflective j] : j.FullyFaithful

A coreflective functor is fully faithful.

theorem CategoryTheory.counit_obj_eq_map_counit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (j : Functor C D) [Coreflective j] (X : D) : (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) = j.map ((coreflector j).map ((coreflectorAdjunction j).counit.app X))

theorem CategoryTheory.Functor.essImage.counit_isIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {j : Functor C D} [Coreflective j] {A : D} (h : j.essImage A) : IsIso ((coreflectorAdjunction j).counit.app A)

theorem CategoryTheory.mem_essImage_of_counit_isSplitEpi {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {j : Functor C D} [Coreflective j] {A : D} [IsSplitEpi ((coreflectorAdjunction j).counit.app A)] : j.essImage A

@[implicit_reducible]

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