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

Constructing reflective subcategories🔗

Earlier, we saw that any reflective subcategory has an invertible counit. We will now prove the converse: if the counit of an adjunction is invertible, then the left adjoint is a reflector.

Let $\varepsilon^{-1}$ be the (natural) inverse to the counit, and let $f : \mathcal{C}(G(X), G(Y))$ . We can obtain a map $\mathcal{D}(X,Y)$ by conjugating with $\varepsilon$ and its inverse.

  is-counit-iso→is-reflective : is-invertibleⁿ counit → is-reflective adj
  is-counit-iso→is-reflective counit-iso =
    is-iso→is-equiv $
      iso (λ f → counit.ε _ D.∘ F.₁ f D.∘ ε⁻¹ _)

Proving that this conjugation forms an equivalence involves the usual adjoint yoga. For the forward direction, we need to show that $G(\varepsilon \circ F(f) \circ \varepsilon^{-1}) = f$ ; if we take the right adjunct, this transforms our goal into $\varepsilon \circ F(G(\varepsilon \circ F(f) \circ \varepsilon^{-1})) = \varepsilon \circ F(f)$ .

From here, we can repeatedly apply naturality to commute the $\varepsilon$ all the way to the end of the chain of morphisms. This yields $\varepsilon \circ F(f) \circ \varepsilon^{-1} \circ \varepsilon$ , which is equal to $\varepsilon \circ F(f)$ , as $\varepsilon^{-1}$ is an inverse.

        (λ f → Equiv.injective (_ , R-adjunct-is-equiv adj) $
          counit.ε _ D.∘ F.₁ (G.₁ (counit.ε _ D.∘ F.₁ f D.∘ ε⁻¹ _))   ≡⟨ FG.popl (counit .is-natural _ _ _) ⟩
          (counit.ε _ D.∘ counit.ε _) D.∘ F.₁ (G.₁ (F.₁ f D.∘ ε⁻¹ _)) ≡⟨ D.extendr (FG.shufflel (counit .is-natural _ _ _)) ⟩
          (counit.ε _ D.∘ F.₁ f) D.∘ counit.ε _ D.∘ F.₁ (G.₁ (ε⁻¹ _)) ≡⟨ D.elimr (counit .is-natural _ _ _ ∙ counit-iso.invr ηₚ _) ⟩
          counit.ε _ D.∘ F.₁ f ∎)

The reverse direction follows from a quick application of naturality.

        (λ f →
          counit.ε _ D.∘ F.₁ (G.₁ f) D.∘ ε⁻¹ _ ≡⟨ D.pulll (counit.is-natural _ _ _) ⟩
          (f D.∘ counit.ε _) D.∘ ε⁻¹ _         ≡⟨ D.cancelr (counit-iso.invl ηₚ _) ⟩
          f ∎)
    where
      module counit-iso = is-invertibleⁿ counit-iso
      ε⁻¹ = counit-iso.inv .η

Furthermore, if we have any natural isomorphism $\alpha : FG \cong \operatorname{Id}_{}$ , then the left adjoint is a reflector! To show this, we will construct an inverse to the counit; our previous result will then ensure that $F$ is fully faithful.

To begin, recall that isos have the 2-out-of-3 property, so it suffices to show that $\varepsilon \circ \alpha$ is invertible. Next, note that we can transfer the comonad structure on $FG$ onto a comonad structure on $\operatorname{Id}_{}$ by repeatedly composing with $\alpha$ ; this yields a natural transformation $\delta : \operatorname{Id}_{} \to \operatorname{Id}_{}$ that is a right inverse to $\varepsilon \circ \alpha$ .

Finally, all natural transformations $\operatorname{Id}_{} \to \operatorname{Id}_{}$ commute with one another, so $\delta$ is also a right inverse, and $\varepsilon \circ \alpha$ is invertible.

  FG-iso→is-reflective : (F F∘ G) ≅ⁿ Id → is-reflective adj
  FG-iso→is-reflective α =
    is-counit-iso→is-reflective $
    [D,D].invertible-cancell
      ([D,D].iso→invertible (α [D,D].Iso⁻¹))
      ([D,D].make-invertible δ right-ident right-ident⁻¹)
    where
      module α = Isoⁿ α

      δ : Id {C = D} => Id
      δ .η x = α.to .η x D.∘ α.to .η (F.F₀ (G.₀ x)) D.∘ F.₁ (unit.η (G.₀ x)) D.∘ α.from .η x
      δ .is-natural x y f =
        D.extendr (D.extendr (D.extendr (α.from .is-natural _ _ _)))
        ∙ D.pushl (D.pushr (D.pushr (F.weave (unit .is-natural _ _ _))))
        ∙ D.pushl (D.pushr (α.to .is-natural _ _ _))
        ∙ D.pushl (α.to .is-natural _ _ _)

      right-ident : (counit ∘nt α.from) ∘nt δ ≡ idnt
      right-ident = Nat-path λ x →
        D.cancel-inner (α.invr ηₚ _)
        ∙ D.pulll (sym $ α.to .is-natural _ _ _)
        ∙ D.cancel-inner (F.annihilate zag)
        ∙ α.invl ηₚ _

      right-ident⁻¹ : δ ∘nt (counit ∘nt α.from) ≡ idnt
      right-ident⁻¹ = id-nat-commute δ (counit ∘nt α.from) ∙ right-ident