Documentation

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

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.

Instances

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

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 a split monomorphism, then A is in the reflective subcategory.

Composition of reflective functors.

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

The description of the inverse of the bijection unitCompPartialBijectiveAux.

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.

Equations
  • One or more equations did not get rendered due to their size.
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) :
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) :

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.
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.

Instances

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

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