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

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

Instances

    The adjunction reflector i ⊣ i when i is reflective.

    Equations
    Instances For

      A reflective functor is fully faithful.

      Equations
      Instances For

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

        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.
        Instances For
          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 : i.EssImageSubcategory) :
          ((i.essImageInclusion.comp (CategoryTheory.reflector i)).comp i.toEssImage).obj X X

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

          Equations
          Instances For
            @[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_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 = i.essImageInclusion.comp (CategoryTheory.reflector i)
            @[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 = i.toEssImage

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