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 ) 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.
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 = componentwise-invertibleβinvertible counit Ξ» x β D.isoβinvertible (is-reflectiveβcounit-is-iso {o = x})
We can now prove that the adjunction 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 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 -algebra; We will show that as -algebras β 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 = 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