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 Propsβ†ͺSets{{\mathbf{Props}}}{\hookrightarrow}{{\mathbf{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\mathcal{C} as a reflective subcategory of D\mathcal{D}. Reflective subcategory inclusions are of particular importance because they are monadic functors: They exhibit C\mathcal{C} as the category of algebras for an (idempotent) monad on D\mathcal{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 Ρ:FGo→o{\varepsilon}: FGo \to o of a reflexive subcategory inclusion is an isomorphism. Since GG is fully faithful, the unit map ηGo:Go→GFGo\eta_{Go} : Go \to GFGo corresponds to a map o→FGoo \to FGo, and this map can be seen to be a left- and right- inverse to Ρ{\varepsilon} applying the triangle identities.

module
  _ {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²} {F : Functor C D} {G : Functor D C}
    (adj : F ⊣ G) (g-ff : is-reflective adj)
  where
  private
    module DD = Cat.Reasoning Cat[ D , D ]
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module F = Func F
    module G = Func G
    module GF = Func (G F∘ F)
    module FG = Func (F F∘ G)
    module g-ff {x} {y} = Equiv (_ , g-ff {x} {y})
  open _⊣_ adj

  is-reflectiveβ†’counit-is-iso : βˆ€ {o} β†’ FG.β‚€ o D.β‰… o
  is-reflective→counit-is-iso {o} = morp where
    morp : F.β‚€ (G.β‚€ o) D.β‰… o
    morp = D.make-iso (counit.Ξ΅ _) (g-ff.from (unit.Ξ· _)) invl invr
      where abstract
      invl : counit.Ξ΅ o D.∘ g-ff.from (unit.Ξ· (G.β‚€ o)) ≑ D.id
      invl = fully-faithful→faithful {F = G} g-ff (
        G.₁ (counit.Ξ΅ o D.∘ _)                 β‰‘βŸ¨ G.F-∘ _ _ βŸ©β‰‘
        G.₁ (counit.Ξ΅ o) C.∘ G.₁ (g-ff.from _) β‰‘βŸ¨ C.refl⟩∘⟨  g-ff.Ξ΅ _ βŸ©β‰‘
        G.₁ (counit.Ξ΅ o) C.∘ unit.Ξ· (G.β‚€ o)    β‰‘βŸ¨ zag βˆ™ sym G.F-id βŸ©β‰‘
        G.₁ D.id                               ∎)

      invr : g-ff.from (unit.Ξ· (G.β‚€ o)) D.∘ counit.Ξ΅ o ≑ D.id
      invr = fully-faithfulβ†’faithful {F = G} g-ff (ap G.₁ (
        g-ff.from _ D.∘ counit.Ξ΅ _             β‰‘Λ˜βŸ¨ counit.is-natural _ _ _ βŸ©β‰‘Λ˜
        counit.Ξ΅ _ D.∘ F.₁ (G.₁ (g-ff.from _)) β‰‘βŸ¨ D.refl⟩∘⟨ F.⟨ g-ff.Ξ΅ _ ⟩ βŸ©β‰‘
        counit.Ξ΅ _ D.∘ F.₁ (unit.Ξ· _)          β‰‘βŸ¨ zig βŸ©β‰‘
        D.id                                   ∎))

  is-reflectiveβ†’counit-iso : (F F∘ G) DD.β‰… Id
  is-reflective→counit-iso = DD.invertible→iso counit invs where
    invs = componentwise-invertible→invertible counit λ x →
      D.iso→invertible (is-reflective→counit-is-iso {o = x})

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

is-reflective→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 Dβ†’CGFD \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→counit g-ff _)
    isom .linv x = equiv→unit g-ff _

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 o≅GFoo \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 o→GF(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{\varepsilon}_x, which is an isomorphism because Ξ΅{\varepsilon} 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 =
        unit.is-natural _ _ _
      βˆ™ apβ‚‚ C._∘_ refl (Ξ·-comonad-commute adj g-ff)
      βˆ™ sym (G.F-∘ _ _)
      βˆ™ ap G.₁ (sym (F.F-∘ _ _) Β·Β· ap F.₁ (alg .Ξ½-unit) Β·Β· F.F-id)
      βˆ™ sym (apβ‚‚ C._∘_ refl (sym (Ξ·-comonad-commute adj g-ff)) βˆ™ 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 _ (
          unit.is-natural _ _ _
        Β·Β· apβ‚‚ C._∘_ refl (Ξ·-comonad-commute adj g-ff)
        ·· 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