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

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

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\props \mono \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\ca{C} as a reflective subcategory of D\ca{D}. Reflective subcategory inclusions are of particular importance because they are monadic functors: They exhibit C\ca{C} as the category of algebras for an (idempotent) monad on D\ca{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\eps : 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 Ρ\eps applying the triangle identities.

is-reflective→counit-is-iso
  : {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²} {F : Functor C D} {G : Functor D C}
  β†’ (adj : F ⊣ G) β†’ is-reflective adj
  β†’ βˆ€ {o} β†’ Cat.Reasoning._β‰…_ D (Fβ‚€ F (Fβ‚€ G o)) o
is-reflective→counit-is-iso {C = C} {D} {F} {G} adj g-ff {o} = morp where
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D
  module F = Func F
  module G = Func G
  open _⊣_ adj

  morp : F.β‚€ (G.β‚€ o) D.β‰… o
  morp = D.make-iso (counit.Ρ _) (equiv→inverse g-ff (unit.η _)) invl invr
    where abstract
    invl : counit.Ξ΅ o D.∘ equivβ†’inverse g-ff (unit.Ξ· (G.β‚€ o)) ≑ D.id
    invl = fully-faithful→faithful {F = G} g-ff (
      G.₁ (counit.Ξ΅ o D.∘ _)                          β‰‘βŸ¨ G.F-∘ _ _ βŸ©β‰‘
      G.₁ (counit.Ξ΅ o) C.∘ G.₁ (equivβ†’inverse g-ff _) β‰‘βŸ¨ C.refl⟩∘⟨ equivβ†’section g-ff _ βŸ©β‰‘
      G.₁ (counit.Ξ΅ o) C.∘ unit.Ξ· (G.β‚€ o)             β‰‘βŸ¨ zag βˆ™ sym G.F-id βŸ©β‰‘
      G.₁ D.id                                        ∎)

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

is-reflective→counit-iso
  : {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²} {F : Functor C D} {G : Functor D C}
  β†’ (adj : F ⊣ G) β†’ is-reflective adj
  β†’ Cat.Reasoning._β‰…_ Cat[ D , D ] (F F∘ G) Id
is-reflective→counit-iso {C = C} {D} adj ff = DD.invertible→iso counit invs where
  module DD = Cat.Reasoning Cat[ D , D ]
  module D = Cat.Reasoning D
  open _⊣_ adj
  invs = componentwise-invertible→invertible counit λ x →
    D.iso→invertible (is-reflective→counit-is-iso adj ff {o = x})

We can now prove that the adjunction L⊣ι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β†’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→section g-ff _)
    isom .linv x = equiv→retraction g-ff _

  Tunit≑unitT : βˆ€ {x} β†’ unit.Ξ· (G.β‚€ (F.β‚€ x)) ≑ G.₁ (F.₁ (unit.Ξ· x))
  Tunit≑unitT {x} = C.right-inv-unique
    (F-map-iso G (is-reflective→counit-is-iso adj g-ff))
    zag
    (sym (G.F-∘ _ _) βˆ™ ap G.₁ zig βˆ™ G.F-id)

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\eps_x, which is an isomorphism because Ξ΅\eps 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 Tunit≑unitT
      βˆ™ sym (G.F-∘ _ _)
      βˆ™ ap G.₁ (sym (F.F-∘ _ _) Β·Β· ap F.₁ (alg .Ξ½-unit) Β·Β· F.F-id)
      βˆ™ sym (apβ‚‚ C._∘_ refl (sym Tunit≑unitT) βˆ™ 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 Tunit≑unitT
        ·· 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