open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Equivalence
open import Cat.Instances.Functor
open import Cat.Functor.Adjoint
open import Cat.Diagram.Monad
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Functor.Adjoint.Reflective where

Reflective subcategories🔗

Occasionally, full subcategory inclusions (hence fully faithful functors — like the inclusion of abelian groups into the category of all groups, or the inclusion PropsSets\props \mono \sets) participate in an adjunction

When this is the case, we refer to the left adjoint functor LL as the reflector, and ι\iota exhibits C\ca{C} as a reflective subcategory of D\ca{D}. Reflective subcategory inclusions are of particular importance because they are monadic functors: They exhibit C\ca{C} as the category of algebras for an (idempotent) monad on D\ca{D}.

is-reflective : F  G  Type _
is-reflective {G = G} adj = is-fully-faithful G

The first thing we will prove is that the counit map ε:FGoo\eps : FGo \to o of a reflexive subcategory inclusion is an isomorphism. Since GG is fully faithful, the unit map ηGo:GoGFGo\eta_{Go} : Go \to GFGo corresponds to a map oFGoo \to FGo, and this map can be seen to be a left- and right- inverse to ε\eps applying the triangle identities.

  : {C : Precategory o } {D : Precategory o′ ℓ′} {F : Functor C D} {G : Functor D C}
   (adj : F  G)  is-reflective adj
    {o}  Cat.Reasoning._≅_ D (F₀ F (F₀ G o)) o
is-reflective→counit-is-iso {C = C} {D} {F} {G} adj g-ff {o} = morp where
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D
  module F = Func F
  module G = Func G
  open _⊣_ adj

  morp : F.₀ (G.₀ o) D.≅ o
  morp = D.make-iso (counit.ε _) (equiv→inverse g-ff (unit.η _)) invl invr
    where abstract
    invl : counit.ε o D.∘ equiv→inverse g-ff (unit.η (G.₀ o))
    invl = fully-faithful→faithful {F = G} g-ff (
      G.₁ (counit.ε o D.∘ _)                          ≡⟨ G.F-∘ _ _ 
      G.₁ (counit.ε o) C.∘ G.₁ (equiv→inverse g-ff _) ≡⟨ C.refl⟩∘⟨ equiv→section g-ff _ 
      G.₁ (counit.ε o) C.∘ unit.η (G.₀ o)             ≡⟨ zag  sym G.F-id 
      G.₁                                        )

    invr : equiv→inverse g-ff (unit.η (G.₀ o)) D.∘ counit.ε o
    invr = fully-faithful→faithful {F = G} g-ff (ap G.₁ (
      equiv→inverse g-ff _ D.∘ counit.ε _             ≡˘⟨ _ _ _ ≡˘
      counit.ε _ D.∘ F.₁ (G.₁ (equiv→inverse g-ff _)) ≡⟨ D.refl⟩∘⟨ F.⟨ equiv→section g-ff _  
      counit.ε _ D.∘ F.₁ (unit.η _)                   ≡⟨ zig                                            ))

  : {C : Precategory o } {D : Precategory o′ ℓ′} {F : Functor C D} {G : Functor D C}
   (adj : F  G)  is-reflective adj
   Cat.Reasoning._≅_ Cat[ D , D ] (F F∘ G) Id
is-reflective→counit-iso {C = C} {D} adj ff = DD.invertible→iso counit invs where
  module DD = Cat.Reasoning Cat[ D , D ]
  module D = Cat.Reasoning D
  open _⊣_ adj
  invs = componentwise-invertible→invertible counit λ x 
    D.iso→invertible (is-reflective→counit-is-iso adj ff {o = x})

We can now prove that the adjunction LιL \dashv \iota is monadic.

  :  {F : Functor C D} {G : Functor D C}
   (adj : F  G)  is-reflective adj  is-monadic adj
is-reflective→is-monadic {C = C} {D = D} {F = F} {G} adj g-ff = eqv where

It suffices to show that the comparison functor DCGFD \to C^GF is fully faithful and split essentially surjective. For full faithfulness, observe that it’s always faithful; The fullness comes from the assumption that GG is ff.

  comp-ff : is-fully-faithful Comp
  comp-ff {x} {y} = is-iso→is-equiv isom where
    open is-iso
    isom : is-iso _
    isom .inv alg = equiv→inverse g-ff (alg .morphism)
    isom .rinv x = Algebra-hom-path _ (equiv→section g-ff _)
    isom .linv x = equiv→retraction g-ff _

  Tunit≡unitT :  {x}  unit.η (G.₀ (F.₀ x))  G.₁ (F.₁ (unit.η x))
  Tunit≡unitT {x} = C.right-inv-unique
    (F-map-iso G (is-reflective→counit-is-iso adj g-ff))
    (sym (G.F-∘ _ _)  ap G.₁ zig  G.F-id)

To show that the comparison functor is split essentially surjective, suppose we have an object oo admitting the structure of an GFGF-algebra; We will show that oGFoo \cong GFo as GFGF-algebras — note that GF(o)GF(o) admits a canonical (free) algebra structure. The algebra map ν:GF(o)o\nu : GF(o) \to o provides an algebra morphism from GF(o)oGF(o) \to o, and the morphism oGF(o)o \to GF(o) is can be taken to be adjunction unit η\eta.

The crucial lemma in establishing that these are inverses is that ηGFx=GF(ηx)\eta_{GFx} = GF(\eta_x), which follows because both of those morphisms are right inverses to GεxG\eps_x, which is an isomorphism because ε\eps is.

  comp-seso : is-split-eso Comp
  comp-seso (ob , alg) = F.₀ ob , isom where
    Fo→o : Algebra-hom _ (L∘R adj) (Comp.₀ (F.₀ ob)) (ob , alg)
    Fo→o .morphism = alg .ν
    Fo→o .commutes = sym (alg .ν-mult)

    o→Fo : Algebra-hom _ (L∘R adj) (ob , alg) (Comp.₀ (F.₀ ob))
    o→Fo .morphism = unit.η _
    o→Fo .commutes = _ _ _
       ap₂ C._∘_ refl Tunit≡unitT
       sym (G.F-∘ _ _)
       ap G.₁ (sym (F.F-∘ _ _) ·· ap F.₁ (alg .ν-unit) ·· F.F-id)
       sym (ap₂ C._∘_ refl (sym Tunit≡unitT)  zag  sym G.F-id)

    isom : Comp.₀ (F.₀ ob) EM.≅ (ob , alg)
    isom = EM.make-iso Fo→o o→Fo
      (Algebra-hom-path _ (alg .ν-unit))
      (Algebra-hom-path _ (
 _ _ _
        ·· ap₂ C._∘_ refl Tunit≡unitT
        ·· sym (G.F-∘ _ _)
        ·· ap G.₁ (sym (F.F-∘ _ _) ·· ap F.₁ (alg .ν-unit) ·· F.F-id)
        ·· G.F-id))

  eqv : is-equivalence Comp
  eqv = ff+split-eso→is-equivalence comp-ff comp-seso