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 participate in an adjunction

When this is the case, we refer to the left adjoint functor as the reflector, and exhibits as a reflective subcategory of Reflective subcategory inclusions are of particular importance because they are monadic functors: They exhibit as the category of algebras for an (idempotent) monad on

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 of a reflexive subcategory inclusion is an isomorphism. Since is fully faithful, the unit map corresponds to a map and this map can be seen to be a left- and right- inverse to 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 (ε _) (g-ff.from (unit.η _)) invl invr
      where abstract
      invl : ε o D.∘ g-ff.from (unit.η (G.₀ o)) ≡
      invl = fully-faithful→faithful {F = G} g-ff (
        G.₁ (ε o D.∘ _)                 ≡⟚ G.F-∘ _ _ ⟩≡
        G.₁ (ε o) C.∘ G.₁ (g-ff.from _) ≡⟚ C.refl⟩∘⟚  g-ff.ε _ ⟩≡
        G.₁ (ε o) C.∘ unit.η (G.₀ o)    ≡⟚ zag ∙ sym G.F-id ⟩≡
        G.₁                        ∎)

      invr : g-ff.from (unit.η (G.₀ o)) D.∘ ε o ≡
      invr = fully-faithful→faithful {F = G} g-ff (ap G.₁ (
        g-ff.from _ D.∘ ε _             ≡˘⟚ _ _ _ ⟩≡˘
        ε _ D.∘ F.₁ (G.₁ (g-ff.from _)) ≡⟚ D.refl⟩∘⟚ F.⟹ g-ff.ε _ ⟩ ⟩≡
        ε _ 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 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 is fully faithful and split essentially surjective. For full faithfulness, observe that it’s always faithful; The fullness comes from the assumption that 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 admitting the structure of an We will show that as — note that admits a canonical (free) algebra structure. The algebra map provides an algebra morphism from and the morphism is can be taken to be adjunction unit

The crucial lemma in establishing that these are inverses is that which follows because both of those morphisms are right inverses to which is an isomorphism because 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

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 be the (natural) inverse to the counit, and let We can obtain a map by conjugating with 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 → ε _ 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 if we take the right adjunct, this transforms our goal into

From here, we can repeatedly apply naturality to commute the all the way to the end of the chain of morphisms. This yields which is equal to as is an inverse.

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

The reverse direction follows from a quick application of naturality.

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

Furthermore, if we have any natural isomorphism 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 is fully faithful.

To begin, recall that isos have the 2-out-of-3 property, so it suffices to show that is invertible. Next, note that we can transfer the comonad structure on onto a comonad structure on by repeatedly composing with this yields a natural transformation that is a right inverse to

Finally, all natural transformations commute with one another, so is also a right inverse, and is invertible.

  FG-iso→is-reflective : (F F∘ G) ≅ⁿ Id → is-reflective adj
  FG-iso→is-reflective α =
    is-counit-iso→is-reflective $
      ([D,D].iso→invertible (α [D,D].Iso⁻¹))
      ([D,D].make-invertible Ύ right-ident right-ident⁻¹)
      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 = ext λ 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