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

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



# 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 ${{\mathbf{Props}}}{\hookrightarrow}{{\mathbf{Sets}}}$) participate in an adjunction  When this is the case, we refer to the left adjoint functor $L$ as the reflector, and $\iota$ exhibits $\mathcal{C}$ as a reflective subcategory of $\mathcal{D}$. Reflective subcategory inclusions are of particular importance because they are monadic functors: They exhibit $\mathcal{C}$ as the category of algebras for an (idempotent) monad on $\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 ${\varepsilon}: FGo \to o$ of a reflexive subcategory inclusion is an isomorphism. Since $G$ is fully faithful, the unit map $\eta_{Go} : Go \to GFGo$ corresponds to a map $o \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}
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})

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 \dashv \iota$ is monadic.

is-reflective→is-monadic
: ∀ {F : Functor C D} {G : Functor D C}
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 \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 $G$ 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 $o$ admitting the structure of an $GF$-algebra; We will show that $o \cong GFo$ as $GF$-algebras — note that $GF(o)$ admits a canonical (free) algebra structure. The algebra map $\nu : GF(o) \to o$ provides an algebra morphism from $GF(o) \to o$, and the morphism $o \to GF(o)$ is can be taken to be adjunction unit $\eta$.

The crucial lemma in establishing that these are inverses is that $\eta_{GFx} = GF(\eta_x)$, which follows because both of those morphisms are right inverses to $G{\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 _ _ _
∙ 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 _ _ _