module Cat.Functor.Adjoint.Reflective where
private variable o oβ² β ββ² : Level C D : Precategory o β F G : Functor C D open Functor open _=>_
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 = invertibleβinvertibleβΏ counit Ξ» x β D.isoβinvertible (is-reflectiveβcounit-is-iso {o = x})
Ξ·-comonad-commute : β {x} β unit.Ξ· (G.β (F.β x)) β‘ G.β (F.β (unit.Ξ· x)) Ξ·-comonad-commute {x} = C.right-inv-unique (F-map-iso G is-reflectiveβcounit-is-iso) zag (sym (G.F-β _ _) β ap G.β zig β G.F-id) is-reflectiveβunit-G-is-iso : β {o} β C.is-invertible (unit.Ξ· (G.β o)) is-reflectiveβunit-G-is-iso {o} = C.make-invertible (g-ff.to (counit.Ξ΅ _)) (unit.is-natural _ _ _ Β·Β· apβ C._β_ refl Ξ·-comonad-commute Β·Β· GF.annihilate zag) zag is-reflectiveβF-unit-is-iso : β {o} β D.is-invertible (F.β (unit.Ξ· o)) is-reflectiveβF-unit-is-iso {o} = D.make-invertible (counit.Ξ΅ _) (sym (counit.is-natural _ _ _) β apβ D._β_ refl (ap F.β (sym Ξ·-comonad-commute)) β zig) zig
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
module EM = Cat.Reasoning (Eilenberg-Moore C (LβR adj)) module C = Cat.Reasoning C module D = Cat.Reasoning D module F = Functor F module G = Functor G open Algebra-hom open Algebra-on open _β£_ adj Comp : Functor D (Eilenberg-Moore C (LβR adj)) Comp = Comparison adj module Comp = Functor Comp
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