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 $\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}
    (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 = 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}
  → (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 \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 _ _ _
      ∙ 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