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.

  _ {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²} {F : Functor C D} {G : Functor D C}
    (adj : F ⊣ G) (g-ff : is-reflective adj)
    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)) ≑
      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.₁                               ∎)

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

  is-reflectiveβ†’counit-iso : (F F∘ G) DD.β‰… Id
  is-reflective→counit-iso = DD.invertible→iso counit invs where
    invs = 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.

  : βˆ€ {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 = _ _ _
      βˆ™ 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 _ (
 _ _ _
        Β·Β· 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